Binary Search Invariants: A Formal Treatment

Binary search is often taught as a pattern to memorize. This paper gives a formal treatment using loop invariants, so you can derive correct implementations and avoid off-by-one errors.

The Problem

Given a sorted array $A[0..n-1]$ and a value $v$, find index $i$ such that $A[i] = v$, or determine that $v$ is not present.

The Invariant

We maintain indices $lo$ and $hi$ such that:

1. Invariant: If $v$ is in $A$, then $v \in A[lo..hi]$.
2. Bounds: $0 \leq lo \leq hi < n$ (or $hi = -1$ when the range is empty).

Initially, $lo = 0$ and $hi = n - 1$, so the invariant holds: the full array contains $v$ if it exists.

The Loop

Each iteration computes $mid = \lfloor (lo + hi) / 2 \rfloor$ and compares $A[mid]$ with $v$:

• If $A[mid] = v$, we return $mid$.
• If $A[mid] < v$, then $v$ cannot be in $A[0..mid]$ (array is sorted). Set $lo = mid + 1$.
• If $A[mid] > v$, then $v$ cannot be in $A[mid..n-1]$. Set $hi = mid - 1$.

In each case, we shrink the range while preserving the invariant. When $lo > hi$, the range is empty and $v$ is not in the array.

Termination

The quantity $hi - lo + 1$ (the size of the search range) decreases by at least 1 each iteration. It starts non-negative, so the loop terminates.

Implementation

def binary_search(A: list[int], v: int) -> int:
    lo, hi = 0, len(A) - 1
    while lo <= hi:
        mid = (lo + hi) // 2
        if A[mid] == v:
            return mid
        if A[mid] < v:
            lo = mid + 1
        else:
            hi = mid - 1
    return -1

The invariant guides the implementation. No memorization required.