Loop Invariants

A loop is where program proofs get hard. A straight-line block of code has finitely many statements, so you can reason through them one at a time; a loop compresses an unbounded number of steps into a few lines, and you cannot unroll it to check each iteration — there might be a billion. The trick that tames it is one of the most beautiful ideas in computer science: find a single assertion that is true every time you reach the top of the loop, no matter how many times round you have been. That assertion is the loop invariant, and it lets you prove something about an unbounded process by checking just one generic iteration.

This is the same move as mathematical induction, and it slots directly into Hoare logic as the rule for while. Get the invariant right and the correctness of the loop falls out almost mechanically; get it wrong and no amount of staring at the code will save you.

The Hoare while-rule

The rule for loops is the whole of loop reasoning in one line. If I is preserved by the body whenever the guard b is true, then I survives the whole loop, and on exit you additionally know the guard has failed:

\frac{\{I \wedge b\}\; C \;\{I\}}{\{I\}\; \texttt{while } b \texttt{ do } C \;\{I \wedge \neg b\}}

Read the premise above the line: "starting in a state where I holds and the guard b is true, one execution of the body C restores I." Read the conclusion below: "the loop as a whole takes I in to I \wedge \neg b out." That conjunct \neg b is the payoff — it is the extra fact, gained for free at exit, that you combine with I to reach the postcondition you actually want. Note the rule proves partial correctness only: it says nothing about whether the loop ever exits.

The three-part discipline

In practice we do not manipulate the rule symbolically; we check a good invariant against three concrete obligations. Memorise them as Initialise, Maintain, Conclude — every loop-correctness argument you will ever write is these three boxes ticked.

Initialisation. I is true before the first iteration — i.e. the code that sets up the loop establishes it. (Base case.)
Maintenance. If I is true at the top of the loop and the guard holds, then after one execution of the body I is true again: \{I \wedge b\}\, C\, \{I\}. (Inductive step.)
Conclusion (usefulness). When the loop exits, I \wedge \neg b is strong enough to imply the desired postcondition Q. A true-but-useless invariant (like \texttt{true}) passes the first two and fails this one.

The third box is what separates a correct invariant from a useful one. Any tautology is trivially initialised and maintained; the craft is finding an invariant strong enough that I \wedge \neg b \Rightarrow Q at exit, yet weak enough that the body actually preserves it. That tension — strong enough to conclude, weak enough to maintain — is the entire art of loop invariants.

The analogy to induction

The three obligations are exactly the shape of a proof by induction, iteration by iteration.

Induction on k	Loop invariant
Base case: P(0)	Initialisation: I holds before iteration 0
Inductive step: P(k) \Rightarrow P(k+1)	Maintenance: \{I \wedge b\}\,C\,\{I\}
Conclusion: \forall k.\, P(k)	Conclusion: I holds at every top-of-loop, so at exit

The invariant I plays the role of the induction hypothesis P(k), where k counts iterations. "The invariant holds after k iterations for all k" is literally a theorem proved by induction on k — initialisation is the base case, maintenance is the inductive step. Understanding a loop invariant is understanding induction applied to the flow of a program.

Worked example: summing 1 to n

A loop that accumulates 1 + 2 + \cdots + n. We want the postcondition s = \tfrac{n(n+1)}{2}. The invariant captures "what has been summed so far": after processing up to i-1, s holds their sum.

function sumTo(n: number): number { let s = 0; let i = 1; // invariant I: s === (i - 1) * i / 2 AND 1 <= i <= n + 1 while (i <= n) { s = s + i; i = i + 1; } // exit: i === n + 1, so s === n * (n + 1) / 2 return s; }

Take I:\; s = \tfrac{(i-1)i}{2}. Initialise: before the loop s = 0, i = 1, and \tfrac{(1-1)\cdot 1}{2} = 0 — holds. Maintain: assume s = \tfrac{(i-1)i}{2}; the body does s := s + i then i := i + 1, giving new s' = \tfrac{(i-1)i}{2} + i = \tfrac{i(i+1)}{2} and i' = i+1, so s' = \tfrac{(i'-1)i'}{2} — invariant restored. Conclude: the guard fails when i = n+1, and then I gives s = \tfrac{n(n+1)}{2} — the postcondition. The state trace makes the maintenance step visible for n = 4:

Point	i	s	I:\; s = \tfrac{(i-1)i}{2}
before loop	1	0	0 = 0 ✓
top of iter 1	1	0	0 = 0 ✓
top of iter 2	2	1	1 = 1 ✓
top of iter 3	3	3	3 = 3 ✓
top of iter 4	4	6	6 = 6 ✓
exit (guard fails)	5	10	10 = \tfrac{4\cdot 5}{2} ✓

How to FIND an invariant

Students often feel the invariant is pulled out of a hat. It is not — there are systematic moves for deriving one from the postcondition you are aiming at.

Replace a constant by a variable. The postcondition of the sum loop is s = \tfrac{n(n+1)}{2}. Replace the fixed bound n by the loop variable: s = \tfrac{(i-1)i}{2}. The invariant is the postcondition with the "how far we've got" constant generalised to the running index.
Weaken the postcondition until the loop can maintain it. Take the goal Q and split it into "the part done so far" plus "the part still to do." The invariant is "the part done so far is correct." At exit, "still to do" is empty, so the invariant collapses to Q. This is why a good invariant usually looks like a partially-completed version of the answer.

Worked example: integer exponentiation

Compute b^e by repeated multiplication. Aim for postcondition r = b^{e}. Apply "replace a constant by a variable": introduce a counter k and let the invariant say r = b^{k} so far, counting up to e.

function power(b: number, e: number): number { // precondition: e >= 0 let r = 1; let k = 0; // invariant I: r === b**k AND 0 <= k <= e while (k < e) { r = r * b; k = k + 1; } // exit: k === e, so r === b**e return r; }

Initialise: r = 1 = b^0 with k = 0 — holds. Maintain: if r = b^k, then after r := r \cdot b and k := k+1 we have r = b^k \cdot b = b^{k+1} = b^{k'} — restored. Conclude: the guard fails at k = e, so I gives r = b^{e}. Notice the invariant r = b^k is just the postcondition r = b^e with the constant e replaced by the variable k — exactly the first heuristic in action.

Beginners often forget that on exit you know two things, not one. The invariant I is only half the story; the loop also stopped, which means the guard is now false — that is the \neg b conjunct. Almost every loop proof clicks shut precisely at the junction I \wedge \neg b: the invariant says "I've computed the partial answer correctly up to here," and \neg b says "and here is the whole way." In the sum loop, I is s = \tfrac{(i-1)i}{2} and \neg b is i > n; combined with i \le n+1 from the invariant, i is pinned to exactly n+1, and only then does s = \tfrac{n(n+1)}{2} pop out. If your invariant plus the negated guard does not give the postcondition, the invariant is too weak — strengthen it.

The number-one mistake is to pick an invariant that is easy to maintain but says nothing useful. The assertion I = \texttt{true} is initialised (trivially) and maintained (trivially) by any loop — it sails through the first two obligations. But at exit it gives you only \texttt{true} \wedge \neg b, which is just \neg b, and that is almost never your postcondition. A valid loop invariant is not just any preserved property; it must be strong enough to conclude — obligation three. Symmetrically, do not over-shoot: an invariant so strong that the body breaks it fails maintenance. The sweet spot is a partially-built version of the answer: strong enough that I \wedge \neg b \Rightarrow Q, weak enough that \{I \wedge b\}\,C\,\{I\}. If you only remember one thing: an invariant that passes Initialise and Maintain but fails Conclude has taught you nothing about correctness.