Card 03/ 09
The Invariant That Makes Binary Search Correct
If the target is anywhere, it is between low and high, and every step keeps that true.
A loop invariant is a statement that is true before every iteration of a loop, and binary search's is this: if the target is anywhere in the array, its index lies between low and high, inclusive. This card shows how each step keeps that statement true, why it makes the bounds move to mid + 1 and mid - 1, and why it guarantees the loop ends with the right answer. You use it whenever you write or debug a binary search, because nearly every bug in one breaks it.
Take a search for 30 in 4 9 15 21 28 37 44 52. Before the first step the invariant holds trivially, since low and high cover the whole array. The table checks that each step keeps it.
| Step | Comparison | Bound moved | Why the target cannot be in the discarded half |
|---|---|---|---|
| 1 | Index 3 holds 21, smaller than 30 | low from 0 to 4 | The array is sorted, so indices 0 to 3 hold 21 or less |
| 2 | Index 5 holds 37, larger than 30 | high from 7 to 4 | Indices 5 to 7 hold 37 or more |
| 3 | Index 4 holds 28, smaller than 30 | low from 4 to 5 | Index 4 holds 28, and everything left of it was already discarded |
The bounds move past mid, not onto it, because mid has just been checked and is not the target, so excluding it keeps the invariant true. Excluding it also makes the range strictly shorter at every step, which is what ends the loop. Eventually low passes high and the range is empty; an empty range holds nothing, so by the invariant the target is nowhere in the array and returning -1 is correct. If the target is present, every range still contains it, and since the range cannot shrink for ever, some step lands mid on it.
That gives two questions to ask of any binary search: does every branch keep the invariant, and does every branch make the range shorter? A branch that fails the first returns wrong answers, and one that fails the second never stops. A run on the same array produced both. A version that moved high when the middle item was too small, moving the wrong bound, read indices 3, 1 and 0 while searching for 44 and returned -1, although 44 sits at index 6: its first step discarded the half that held the target. A version that set low = mid and high = mid searched for 30 until it reached low 4, mid 4, high 5, and was still in that state after six iterations, because when mid equals low, setting low = mid moves nothing.
The invariant is how a binary search is written correctly the first time rather than tested into shape: decide what low and high mean, then make every line keep that meaning.
← → move through sections and cards