The invariant

Binary search is easy to describe, but it is easy to get wrong in code. Being extra careful with the + 1 and - 1 is not enough. The reliable way is to write down one statement that stays true for the whole loop, and then prove that it does.

The statement we keep true

A statement that stays true every time a loop runs is called a loop invariant. For binary search, it is this:

Read it carefully. It does not say that t is in the window, because t may not be in the list at all. It says that the window never loses t. Every position outside a[lo..hi] has been proved not to hold t. That is what the shaded cells in the figures mean. They do not mean “we have not looked there”. They mean “we know t is not there”.

Proving the loop is correct

We prove a loop invariant in three parts. (The Correctness station covers this method in general.)

def search(a, t):
    lo, hi = 0, len(a) - 1          # start: the window is all of a
    while lo <= hi:
        mid = (lo + hi) // 2        # lo <= mid <= hi
        if a[mid] == t:
            return mid
        elif a[mid] < t:
            lo = mid + 1            # a[lo..mid] are all < t
        else:
            hi = mid - 1            # a[mid..hi] are all > t
    return -1                       # empty window: t is not in a

1. It is true at the start. With lo = 0 and hi = n - 1, the window is the whole list. If t is in a, it is in the window.
2. Each pass keeps it true. Suppose it is true at the start of a pass, and a[mid] < t. The list is sorted, so every value from a[lo] to a[mid] is at most a[mid], which is less than t. None of them can be t. So if t was in a[lo..hi], it is in a[mid+1..hi]. Setting lo = mid + 1 keeps the statement true. The case a[mid] > t works the same way on the other side.
3. It gives the right answer at the end. The loop ends in one of two ways. Either it returns mid with a[mid] == t, which is clearly right. Or the window is empty, because lo > hi. An empty window holds nothing, so by the invariant t is not in a, and -1 is the right answer.

The proof used three facts: a is sorted, mid is inside the window, and each branch removes only positions that cannot hold t. If you change any line of the code, you can check which part of the proof still holds.

Why the loop stops

A correct invariant is not enough on its own. A loop that never ends never gives a wrong answer, but it is still broken. We also need to show that the loop stops. To do that, find a whole number that gets smaller on every pass and can never go below zero.

Here, that number is the size of the window, hi − lo + 1. Since lo ≤ mid ≤ hi, both updates remove mid from the window. So the window gets at least one smaller on every pass. A whole number that keeps getting smaller, and cannot go below zero, must stop. So the loop ends.

Breaking it on purpose

Here is a bug that looks harmless. Someone shortens the code to two branches and removes the equality check:

while lo <= hi:
    mid = (lo + hi) // 2
    if a[mid] < t:
        lo = mid + 1
    else:
        hi = mid - 1        # also runs when a[mid] == t
return -1

Where does the proof fail? In part 2, when a[mid] == t. The else branch removes mid, which is the one position that holds t. Switch the figure below to the buggy version, and step until the window loses the target. The invariant check turns red at that exact step, long before the wrong answer appears.

This is a good habit to build. When a binary search gives a wrong answer, do not change the indices at random until the tests pass. Write down the invariant, and find the line where it stops being true.