The tray on the ladder: one true thing that never tips over
The previous guide left us with a demand we could not yet meet: a loop runs some number of times that depends on the input, so how can we argue about what it produces on every input at once? Tracing one example only tells you about that example — and we already agreed that tests are not proofs. The answer is to stop tracking the constantly-changing state and instead name one thing that stays true through all the churn. That one thing is a loop invariant.
Picture climbing a ladder while balancing a tray of tea. The useful thing to keep saying is not "which rung am I on?" — that changes every step and tells you little. The useful thing is "the tray is still level." If the tray is level before your first step, and every single step keeps it level, then it is still level at the top, no matter how many rungs there were. A loop invariant is exactly that level-tray statement: a property of the program's variables that is true at the loop boundary on every pass, chosen so that when the climb ends it tells you what you accomplished.
The deep idea is that an invariant converts an unbounded question ("what happens over all the iterations?") into a bounded one ("what does one iteration do to this one statement?"). You never reason about the whole run at once; you reason about a single step, and a structural principle stitches those single steps into a guarantee for the whole loop. That principle is induction, and the rest of this guide is about spelling it out cleanly enough to trust.
Three obligations: initialization, maintenance, termination
To use an invariant you must discharge exactly three obligations. Initialization: the invariant is true just before the loop runs for the first time. Maintenance: if the invariant is true at the top of an iteration, the body leaves it true at the top of the next one. Termination: when the loop finally exits, the invariant — combined with the reason it exited — gives you the result you wanted. Get all three and the loop is proven correct (assuming it stops, which we will return to).
Notice the careful wording of maintenance: you assume the invariant for the current iteration only and prove it again for the next. You are emphatically not allowed to assume the final answer, nor the invariant for some later pass — that would be assuming what you are trying to prove. You assume one rung's level tray and show your single step keeps it level on the next rung. This local, one-step character is what makes the obligation checkable: you only have to stare at the loop body and the data, never at the whole unbounded run.
Why it works: a loop invariant is induction in disguise
The three obligations are not an arbitrary checklist; they are mathematical induction wearing programmer's clothing. Let P(k) be the statement "the invariant holds at the top of iteration k." Initialization is the base case P(0): true before the first pass. Maintenance is the inductive step: P(k) implies P(k+1), because the body carries the invariant from one boundary to the next. By induction, P(k) holds for every k — the invariant is true at the start of every iteration, however many there turn out to be. That is the whole reason the level tray is guaranteed level all the way up.
Seeing the equivalence pays off in both directions. It tells you why you may skip the base case at your peril: an inductive step with no true base proves nothing, exactly as a maintenance argument with a false initialization proves nothing — the dominoes never start falling. And it tells you the termination obligation is doing something induction alone does not: it cashes the per-iteration promise into a statement about the final state by adding one more fact, the negated loop condition. Induction keeps the tray level; the exit condition tells you which shelf you set it down on.
A worked micro-proof: summing an array
Let us run the whole machine on the smallest honest example. We want to sum an array A of n numbers. The loop keeps a running total s and a next index i. Before stating any obligation, we commit to one invariant, and the art is choosing it well: not "s is some partial sum" (too vague) but the precise claim that ties s to exactly which elements have been added.
s = 0
i = 1
while i <= n: # invariant: s == sum of A[1..i-1]
s = s + A[i]
i = i + 1
return s- Initialization. Before the first pass, i = 1 and s = 0. The invariant claims s equals the sum of A[1..0], an empty range whose sum is 0. So s = 0 matches, and the invariant holds — established by looking at no elements, which is exactly right.
- Maintenance. Assume at the top of some iteration that s == sum of A[1..i-1]. The body runs s = s + A[i], so now s == sum of A[1..i]; then i = i + 1, so in terms of the new i this reads s == sum of A[1..(new i)-1]. The invariant is re-established for the next boundary, using only the hypothesis for this iteration.
- Termination. The loop continues while i <= n, so it exits precisely when i = n + 1. Substituting that exact exit value into the invariant gives s == sum of A[1..n] — the sum of the entire array, which is what we set out to compute. Reading the boundary as n+1 (not n) is the honest move that catches off-by-one errors.
What an invariant proves — and what it leaves out
Read the sum proof's termination line again and notice a hidden assumption: "the loop exits when i = n+1." We assumed it exits. The three invariant obligations, all together, only prove a conditional: IF the loop stops, the result is correct. They say nothing about whether it stops at all. This weaker guarantee has a name — it is partial correctness. A loop that runs forever is, absurdly, partially correct, because it never produces a wrong answer (it produces no answer).
To upgrade to total correctness — the loop stops and the answer is right — you need a second, separate argument that the loop must halt. The standard tool is a decreasing measure: a non-negative integer attached to the state that strictly drops every iteration. In the sum loop that measure is n - i + 1, the number of iterations still to come; it starts at n, falls by one each pass, and a non-negative integer cannot fall forever, so the loop must reach the exit. Guide 4 of this rung is devoted to building these measures; for now just hold the split firmly.
So the full picture is a clean sum: total correctness = partial correctness (an invariant, proven by induction) + termination (a decreasing measure). The same template scales from this toy to the classics. In insertion sort the invariant is "the prefix A[1..i-1] is sorted and holds the original first i-1 elements," and the loop index supplies the measure; in a binary search the invariant pins the target to a shrinking window and that window's width is the measure. Master the trio on the sum loop and you have the skeleton of every loop proof you will meet on the way up this ladder.