二分搜尋的不變量證明（binary-search invariant proof）
二分搜尋在已排序陣列中找一個值的方式，是反覆把搜尋窗口減半：看中間元素，由於陣列已排序，一次比較就能丟掉半個窗口。它出了名地好寫，也出了名地容易在細節上寫錯——邊界差一與無窮迴圈比比皆是。一個乾淨的不變量證明，正是讓你能信任的二分搜尋與「只是通過了你測試」的二分搜尋之間的分水嶺。
維護一個可能仍含目標 x 的索引窗口 [lo, hi]。迴圈不變量是：若 x 在陣列中的任何地方，則 x 落在 A[lo..hi] 內。初始化：令 lo = 1、hi = n，於是窗口是整個陣列；顯然若 x 存在，它就在 A[1..n] 中。維持：計算 mid；因為陣列已排序，若 A[mid] < x，則 x（若存在）必在右側，故設 lo = mid + 1，捨棄不可能含 x 的 A[lo..mid]；對稱地，若 A[mid] > x 則設 hi = mid - 1；若 A[mid] = x 則已找到並停止。在每個分支中，不變量都在更小的窗口上被保住。終止：度量 hi - lo + 1 每步嚴格遞減（因為 mid 嚴格在窗口內部，而我們總是排除它），故迴圈會結束——要嘛找到 x，要嘛在 lo > hi 時結束、意指窗口為空；由不變量，此時 x 不在陣列中任何地方，所以回報「不存在」是正確的。
這個證明釘住了實務上會出錯的全部三件事。不變量逼你選 lo = mid + 1（而非 mid），這正是防止無窮迴圈的關鍵；終止度量證明迴圈真的會結束；而離開條件 lo > hi 正是「找不到」答案的依據。輸入的已排序性是整個論證所倚賴的前置條件——在未排序的陣列上，「丟掉半個窗口」沒有依據，二分搜尋根本就是錯的，不論它怎麼寫。
在 [1, 3, 5, 7, 9, 11] 中搜尋 7。窗口 [1,6]，mid=3（值 5）< 7 -> lo=4。窗口 [4,6]，mid=5（值 9）> 7 -> hi=4。窗口 [4,4]，mid=4（值 7）= 7 -> 找到。窗口每步嚴格縮小 6 -> 3 -> 1，而目標自始至終都待在窗口內，正如不變量所承諾。
不變量：「若 x 存在則它在 [lo, hi] 中」；度量 hi-lo+1 縮小到被迫離開。
已排序是證明所依賴的前置條件；在未排序陣列上，二分搜尋無論怎麼寫都是錯的。選 lo = mid+1／hi = mid-1（排除 mid）正是保證度量嚴格遞減、迴圈會終止的關鍵。