for the few of us.

已知兩整數 M < N 使得 Φ(M,N) 成立。上次我們介紹了 Netty van Gasteren 和 Wim Feijen 的二元搜尋法，能找到某個 l, M ≤ l < N，使得 Φ(l,l+1) 成立。給定一個排序好的陣列 a[0..N)（其元素為 a[0], a[1] ... a[N-1]）, 0 ≤ N。如何用 van Gasteren 與 Feijen 的方法判斷其中是否含有某個關鍵值 K 呢？

第一個念頭是用這個 Φ:

Φ(i,j) = a[i] ≤ K < a[j]

並令 M = 0。演算法結束後，Φ(l,l+1) = a[l] ≤ K < a[l+1] 一定成立，只要再看看 a[l] 是否等於 K 就可以了。但問題來了：van Gasteren-Feijen 演算法正確的兩個先決條件之一是 M < N -- van Gasteren-Feijen 演算法的迴圈設計便假設 [M,N) 這個區段不是空的，因此我們無法處理空陣列。其次是 Φ(0,N) 得要成立，但 a[0] ≤ K < a[N] 並不一定成立呢。

我們可以把上述的例外都分開測試。但 van Gasteren 與 Feijen 建議的作法是在陣列頭尾各補一個想像元素：a[-1] 小於任何數，a[N] 大於任何數。一個等價的說法是用這個Φ:

Φ(i,j)  =  (i = -1  ∨  a[i] ≤ K)  ∧  (K < a[j]  ∨  j = N)

最初令 l, r := -1, N, 那麼初始條件就滿足了。程式如下：

  { 0 ≤ N ∧ Φ(-1,N) }
  l, r := -1, N
  { Inv: -1 ≤ l < r ≤ N  ∧  Φ(l,r),   Bound: r - l }
; do l+1 ≠ r →
    { l + 2 < r }
    m := (l + r) / 2
  ; if a[m] ≤ K → l := m
    [] K < a[m] → r := m
    fi
  od
  { -1 ≤ l < N  ∧  Φ(l,l+1) }
; if l > -1 → found := a[l] = K
  [] l = -1 → found := false
  fi

如果在陣列頭尾補元素讓你覺得很不妥，別擔心。迴圈不變量保證了 -1 < m < N，因此從頭到尾，a[-1] 和 a[N] 兩個位置都沒被讀過 -- 陣列 a 並不用真正有什麼改變，兩個想像元素只是為了證明演算法正確而假想出來的。這也讓我們可以處理空陣列了。我覺得這是 van Gasteren-Feijen 演算法漂亮之處。

Bentley 的程式

Jon Bentley 在 Programming Pearls 一書中給的二元搜尋法程式如果翻譯成 guarded command language, 並把陣列索引從 [1..N] 改成 [0..N-1], 大約是這樣：

  l, r := 0, N-1
; do l ≤ r →
    m := (l + r) / 2
  ; if a[m] < K → l := m + 1
    [] a[m] = K → found := true; break
    [] K < a[m] → r := m - 1
    fi
  od
; found := false

Bentley 書中也有以口語描述的正確性證明。我原想在課堂上講解這個程式，畢竟這個版本流傳較廣 -- 許多函式庫裡的二元搜尋法程式就是這麼寫的。但困難之一是若要把 K < a[m] 和 r := m - 1 牽上關係，似乎非得提早用上陣列已排序好的性質。這個演算法便比較難在更廣泛的脈絡中解釋了。當然，另一個困難是我不知如何在 Hoare logic 中簡單地解釋 break。

乍看之下我以為 Bentley 演算法的搜尋範圍縮小得比 van Gasteren-Feijen 快：l 和 r 分別設為 m+1 與 m-1，並不是 m. 細看之後又發現並不盡然。變數 l 可設為 m+1, 因為 m 的位置已由另一個比較 a[m] = K 處理；變數 r 設為 m-1，則可能僅因為 Bentley 將陣列區段用 a[l..r-1] 表示，而 van Gasteren-Feijen 演算法把同一個區段表達為 a[l..r).

Bentley 與 van Gasteren-Feijen 演算法解的是問題並不完全相同。當 K 在陣列中出現一次以上，Bentley 演算法不限定傳回哪個，van Gasteren-Feijen 則必定傳回索引最大的那個。當 K 不在陣列中時，van Gasteren-Feijen 演算法似乎較快，因為兩者都得跑完，而 van Gasteren-Feijen 的迴圈中只有一個比較（最後一個比較可省去）。Bentley 演算法若提早發現 K 可隨時跳出迴圈，代價是迴圈中多了一個比較。當陣列中確實找得到 K, 這樣的交換是否值得呢？Timothy J. Rolfe 的實驗似乎認為只用一個比較的演算法平均上仍快一些。

習題

Van Gasteren 與 Feijen 建議的幾個習題中包括這個：假設陣列 a[0..N) 是一串嚴格遞增的數字緊接著一串嚴格遞減的數字，試用二元搜尋法找到陣列中的最大值。本問題中我覺得合理的假設是遞增和遞減數列均可能為空的，但 a 至少有一個元素：

0 < N ⋀
(∃ M: 0 ≤ M < N :
  (∀ i,j : 0 ≤ i < j ≤ M : a[i] < a[j]) ⋀
  (∀ i,j : M ≤ i < j < N : a[i] > a[j]))

這剛好是「最大密度區段」問題的演算法之一需要的一個副程式。我記得當時也是先隨便寫寫，幾次寫不對才發現真是難。現在總算是知道一點理論背景，覺得安心多了。你要試試看嗎？

中間索引怎麼取？

關於中間值 m := (l+r)/2, 後來另有些其他故事。Google 的 Joshua Bloch 發現當陣列夠大時，l 和 r 相加可能造成溢位。他可不是故意挑毛病，這個 "bug" 是 Sun 抓到的。他建議該這麼寫：

int m = l + ((r - l) / 2);                          /* for Java/C/C++ */
int m = (l + r) >>> 1;                              /* for Java */
m = ((unsigned int)l + (unsigned int)r)) >> 1;      /* for C/C++ */

Bloch 的發現自然引起了不少討論。有人認為這是整數型別的問題，而不是二元搜尋法的 bug. 有人質疑，討論 int 無法索引的陣列是否有意義？接下來可能一路談到組合語言定址法上頭。有人說，要造成索引溢位，陣列得有 4GB 大，你這輩子在 4GB 的陣列中作二元搜尋過嗎？有人便答，人家可是 Google 來的。Google 的陣列比常人的大上幾倍也不是不可能的唷。

如果往抽象的極端走，Roland Backhouse 在 Program Construction: Calculating Implementations from Specifications 書中則建議應該用 m := (l + r - 1) / 2 -- 如此一來不管該語言的整數除法到底是無條件消去、四捨五入、或是無條件進入，算出來的 m 值都會是 ⌊(l + r)/2⌋.

參考資料

• Roland Backhouse. Program Construction: Calculating Implementations from Specifications. John Wiley and Sons, 2003.
• Jon Bentley. Programming Pearls, Second Edition. Addison-Wesley, 2000.
• Joshua Bloch. Extra, Extra - Read All About It: Nearly All Binary Searches and Mergesorts are Broken. Google Research Blog, June 02, 2006.
• Netty van Gasteren and Wim Feijen. The binary search revisited. AvG127/WF214, 1995.
• Timothy J. Rolfe. Analytic derivation of comparisons in binary search. SIGNUM Newsletter, Vol. 32, No. 4 (Oct 1997), pp. 15-19.

如果你自認對二元搜尋(binary search, 大陸譯作折半搜索) 夠熟悉了，卻沒讀過 Netty van Gasteren 和 Wim Feijen 的研究筆記 The Binary Search Revisited, 強烈建議你找時間看看。

最近為了今夏的 FLOLAC 研習營開始找些資料。為了教些離開研習營後仍有用的東西，今年我想教 Hoare 邏輯與 Dijkstra 使用最弱前提(weakest precondition) 的程式建構法。對想寫好程式的人來說，這應是基礎知識，但大家對這些題目卻陌生得令人驚訝。

二元搜尋似乎是個該談到的例子：給一個排序好、長度為 N 的陣列，在 O(log N) 的時間內決定其中是否有某個值。資訊系學生在演算法課上一定學過二元搜尋。身經百戰的程式員寫個二元搜尋程式應該也不是難事吧？然而 Jon Bentley 在他有名的 Programming Pearls 一書中卻提到只有大約一成的專業程式員能第一次把這程式寫對。這一定要親身試試看才會相信。我抱著警覺心試了一次，寫了一個應該正確（畢竟我對這套方法算是比較熟了），但不怎麼漂亮的程式。請朋友寫寫看，也果然出現了一些常見的 bug. 看來這確實是個程式設計課堂上該講的好例子。

迴圈、不變量、與界限

Van Gasteren 和 Feijen 在一篇 1995 年的研究筆記中釐清了大家常有的一個迷思：你認為你對二元搜尋很了解嗎？那您可知道，二元搜尋其實並不一定要用在排序好的陣列上？事實上，他們認為總是把二元搜尋類比為翻字典找字，反倒造成了一個教學盲點。

Van Gasteren 和 Feijen 先試解一個更廣的問題：給定整數 M 和 N, 和一個接受兩個整數參數的布林函數 Φ，已知 M < N，並知 Φ(M,N) 成立。Φ 另需滿足一些條件，待會兒再談。試寫一個程式，找兩個介於 M 和 N 之間、滿足 Φ 的相鄰整數。若寫成邏輯式子，程式執行完畢後需滿足：

M ≤ l < N   ∧   Φ(l,l+1)

這是 Van Gasteren 和 Feijen 的程式：

  { M < N ∧ Φ(M,N) }
  l, r := M, N
  { Inv: M ≤ l < r ≤ N  ∧  Φ(l,r),   Bound: r - l }
; do l+1 ≠ r →
    { l + 2 < r }
    m := (l + r) / 2
  ; if Φ(m,r) → l := m
    [] Φ(l,m) → r := m
    fi
  od
  { M ≤ l < N  ∧  Φ(l,l+1) }

這裡的虛擬碼使用的是 Dijkstra 的 Guarded Command Language。多個變數可同時設值（如 l, r := M, N），do 相當於 while 迴圈。條件判斷 if 和一般程式語言不同之處是若不只一個條件成立，程式可任選一個分支執行。註解依照 Algol 系語言的傳統用大括號，但此處我們也把註解視作斷言 (assertion), 表示程式執行到此處一定會成立的條件。這是給人看的資訊，也是我們藉以證明程式正確的重要線索。

證明迴圈正確性的兩大關鍵是其不變量 (loop invariant)和界限 (bound)。本程式只有一個迴圈，不變量和界限註記在這一行:

{ Inv: M ≤ l < r ≤ N  ∧  Φ(l,r),   Bound: r - l }

「不變量」事實上並不是一個「量」，而是程式每次執行到迴圈進入點前必定會滿足的條件。此處不變量為 M ≤ l < r ≤ N 和 Φ(l,r)。變數 l 和 r 的初始值分別是 M 和 N. 依照假設，M = l < r = N 和 Φ(l,r) = Φ(M,N) 確實成立。因此第一次執行到迴圈之前，不變量確實是滿足的。

迴圈的進入條件是 l+1 ≠ r，和不變量中的 l < r 合起來看，意思是 l 和 r 不是相鄰的整數。因此m := (l + r) / 2 執行後，m 必定在 l 和 r 之間，但不等於 l 和 r。接下來的 if 敘述中，變數 l 會被設成 m 的先決條件是 Φ(m,r)，變數 r 會被設成 m 的先決條件是 Φ(l,m)。不論是哪種情形，執行完 if 敘述後，Φ(l,r) 一定還是成立。所以再回到迴圈開頭時，不變量仍被滿足。

長此以往，直到有一天剛好 l+1 ≠ r 不成立了，也就是說 l 和 r 已是相鄰的整數，和不變量合起來看，剛好我們要的 結束條件 M ≤ l < N ∧ Φ(l,l+1) 就被滿足了！

只是還有兩個但書：首先，if 敘述中的 Φ(m,r) 和 Φ(l,m) 這兩個條件至少要有一個成立。這是 Φ 的另一個要求：

 Φ(l,r)  ∧  l < m < r   ⇒   Φ(l,m)  ∨  Φ(m,r)(*)

其次，我們怎知道迴圈會有停下來的一天呢？這就是「界限」 r-l 處理的部份。由於 M < N, 我們知道 r-l 最初會是一個正整數。而如前所述，每次進入迴圈後，m 的值必定在 l 和 r 之間，但不等於 l 和 r。因此迴圈每執行一次，r-l 就變小一些。當 r-l 等於一時，迴圈就得停了。因此我們知道這迴圈不可能永遠執行下去。

以上便是該程式正確的大略證明。我們只是用中文說說，更仔細的證明是應該要有些數學演算的。關於什麼算是證明、為何要有「形式」證明，希望以後有機會寫寫看。

有哪些函數 Φ 滿足條件 (*) 呢？ Van Gasteren 與 Feijen 舉的例子包括:

• Φ(i,j) = a[i] ≠ a[j]，此處 a[M..N] 是某陣列。程式會幫我們找到兩個相鄰但不相等的元素。Van Gasteren 與 Feijen 認為這個特例可能是解說二元搜尋比較合適的例子。
• Φ(i,j) = a[i] × a[j] ≤ 0, 程式將找到兩個相鄰但正負號不相等，或至少有一個為零的元素。
• Φ(i,j) = a[i] < a[j],
• Φ(i,j) = a[i] ∨ a[j], 等等。

再回到最初的問題：怎麼在排序好的陣列中找某個關鍵值呢？理想上我們希望設計某個 Φ，然後套用上面的程式。先賣個關子，下回分解。

參考資料

• Roland Backhouse. Program Construction: Calculating Implementations from Specifications. John Wiley and Sons, 2003.
• Jon Bentley. Programming Pearls, Second Edition. Addison-Wesley, 2000.
• Joshua Bloch. Extra, Extra - Read All About It: Nearly All Binary Searches and Mergesorts are Broken. Google Research Blog, June 02, 2006.
• Netty van Gasteren and Wim Feijen. The binary search revisited. AvG127/WF214, 1995.
• Timothy J. Rolfe. Analytic derivation of comparisons in binary search. SIGNUM Newsletter, Vol. 32, No. 4 (Oct 1997), pp. 15-19.