Reviewing a hand-written binary search, which loop invariant convinces you it is correct and terminates?

## What an invariant is, and why this loop needs one A **loop invariant** is a statement about the program's state that is true before the loop starts and true again at the top of every iteration. It is not a comment and not a test; it is the thing you argue about. For a halving search the useful one is: > If the sought value occurs anywhere in the collection, its position lies within the current candidate range. Everything a reviewer needs follows from three obligations attached to that sentence. ### 1. Establishment Before the first iteration the range must cover every position. With an inclusive upper bound that means starting at the last index; with an exclusive one, at the size. This is the obligation people skip, and it is exactly where an initialization that names the wrong end of the collection hides: if the range starts one short, the invariant is false before the loop even runs, and no amount of correct body logic can recover it. The symptom is a silent miss when the answer sits at the excluded end. ### 2. Maintenance Each branch must preserve the invariant. Concretely: the positions the branch throws away must be positions that **cannot** hold the target. In the fragment above, when the midpoint value compares smaller than the target, every position from the lower bound through the midpoint holds a value at most that midpoint value, hence smaller than the target, hence cannot be it — so raising the lower bound past the midpoint preserves the invariant. The mirror argument covers the other branch. Notice what that argument leans on: **the data is ordered under exactly the comparison the code performs**. That premise is the whole justification for discarding half the candidates, and it is the premise that fails in real systems more often than the arithmetic does. Data ordered by one comparison rule and searched by another — different case sensitivity, a locale-aware ordering versus a raw one, a comparison that is not transitive, or values that compare false against everything including themselves — breaks maintenance without breaking anything a debugger shows you. The loop still terminates, still returns, and is simply wrong. When you review a search, ask where the ordering came from and whether the same rule produced it. ### 3. Termination, and what the exit means Two separate things get proved here, and candidates routinely prove only the first. **The loop stops.** Name a measure — the number of remaining candidates — observe it is a non-negative integer, and check *every branch* strictly decreases it. In the inclusive form both branches exclude the midpoint, so the measure falls by at least one unconditionally. In the converging form with an exclusive-style condition, the branch that keeps the midpoint only shrinks the range because the rounding pushes the midpoint strictly away from the bound that branch assigns — which is why the rounding and the shrink step must be chosen as a pair. "It halves each time, so it's logarithmic, so it terminates" is the hand-wave to avoid: halving is a claim about *how fast* the measure falls, and it is only true if the measure falls at all. **The answer at exit is right.** At exit the range is empty and the invariant still holds. Read the invariant with an empty range: *if* the target were present, its position would be inside an empty set — impossible. Therefore it is absent, and returning not-found is justified. This is the step that turns the not-found path from "we ran out of places to look" into a proof, and it is why the invariant must mention presence in the *original* collection rather than merely describing the bounds. ## The predicate form of the same argument The generalisation worth having ready: instead of searching for a value, search for the boundary of a monotone yes/no property — a property false on a prefix of positions and true from some position onward. The invariant becomes: > Everything strictly below the lower bound fails the property; everything at or above the upper bound satisfies it. The loop shrinks the range until the bounds meet, and the meeting point is the boundary. This form makes clear why the ordering premise is really a **monotonicity** premise — sortedness is just the special case where the property is "is at least the target". It is also the form that survives when the search domain is not a stored collection at all: any range of candidate answers over which the property is monotone works the same way, and the invariant is the only thing that tells you so. ## How this reads in a review A useful review script, in order: 1. **Write the invariant above the loop.** If the author cannot state it, the code is a memorised template and the review should be sceptical of every boundary in it. 2. **Check establishment against the initial bounds.** One glance: does the starting range name every position exactly once? 3. **Check each branch against the discard claim.** Annotate what each shrink rules out, as in the fragment above. A branch whose discard cannot be justified in one clause is the bug. 4. **Check the measure falls on every path.** Not "it halves" — falls. 5. **Read the exit condition through the invariant.** Does an empty range genuinely imply absence, and does the code return that? 6. **Trace sizes 0, 1 and 2 by hand.** The invariant argument should already cover them; the trace is a cheap cross-check on the argument itself, and those are the sizes production data eventually supplies and test data usually does not. The reason to prefer this to "I tried a few arrays" is coverage. Random inputs almost never produce a two-candidate range at the exact branch where the rounding bias bites, and never produce the ordering-mismatch case at all. An invariant argument is six lines of reasoning that covers every size and surfaces the premise the tests silently assumed.