the binary-search invariant proof

Binary search finds a value in a sorted array by repeatedly halving the search window: look at the middle element, and because the array is sorted, you can throw away half the window in one comparison. It is famously easy to write and famously easy to get subtly wrong — off-by-one bounds and infinite loops abound. A clean invariant proof is exactly what separates a binary search you can trust from one that merely passes your tests.

Maintain a window [lo, hi] of indices that might still contain the target x. The loop invariant is: if x is anywhere in the array, then x lies within A[lo..hi]. Initialization: set lo = 1, hi = n, so the window is the whole array; trivially if x is present it is in A[1..n]. Maintenance: compute mid; because the array is sorted, if A[mid] < x then x (if present) must be to the right, so set lo = mid + 1, discarding A[lo..mid] which cannot contain x; symmetrically if A[mid] > x set hi = mid - 1; if A[mid] = x we have found it and stop. In every branch the invariant is preserved on the smaller window. Termination: the measure hi - lo + 1 strictly decreases each step (because mid is strictly inside the window and we always exclude it), so the loop ends — either by finding x, or when lo > hi, meaning the window is empty; by the invariant, x is then nowhere in the array, so reporting 'absent' is correct.

This proof pins down all three things that go wrong in practice. The invariant forces you to choose lo = mid + 1 (not mid), which is what prevents an infinite loop; the termination measure proves the loop actually ends; and the exit condition lo > hi is what justifies the 'not found' answer. The sortedness of the input is a precondition the whole argument leans on — on an unsorted array, 'discard half the window' is unjustified and binary search is simply wrong, no matter how it is coded.