Proving a Loop Correct

We have the pieces: a specification as pre- and postconditions, the Hoare while-rule, and the Initialise / Maintain / Conclude discipline for a loop invariant. This page assembles them into a single, complete, end-to-end proof of a non-trivial loop — the kind of argument you would write in a verification report or a viva. We will prove partial correctness: if the loop halts, its answer is right. (Termination is a separate obligation, handled with a variant later in the course.)

The example is integer division by repeated subtraction: given a dividend a \ge 0 and a divisor b > 0, compute the quotient q and remainder r with a = b\,q + r and 0 \le r < b. It is small enough to prove in full, rich enough that the invariant does real work.

The algorithm and its specification

// precondition P: a >= 0 AND b > 0 // postcondition Q: a === b*q + r AND 0 <= r AND r < b function divide(a: number, b: number): { q: number, r: number } { let q = 0; let r = a; // invariant I: a === b*q + r AND 0 <= r while (r >= b) { r = r - b; q = q + 1; } // exit: r < b, and with I this gives Q return { q, r }; }

The idea: start with q = 0 and the whole of a sitting in r; repeatedly peel off one b from r and add one to q. Every peel keeps the total b\,q + r equal to a — that conservation law is the heart of the invariant.

The chosen invariant

We take

I:\quad a = b\,q + r \;\wedge\; 0 \le r.

Where did it come from? Apply the loop-invariant heuristic: the postcondition is a = bq + r \wedge 0 \le r \wedge r < b. Drop the clause the guard will deliver at exit — the guard r \ge b is false on exit, giving exactly r < b — and what remains, a = bq + r \wedge 0 \le r, is the invariant. This is the "weaken the postcondition by the part the loop guard provides" move: the invariant is the goal minus the one fact you get for free by stopping.

Step 1 — Initialisation

Before the loop, the setup code runs q := 0 and r := a. We must show I holds. Substituting:

b \cdot 0 + a = a \;\checkmark \qquad\text{and}\qquad 0 \le a \text{ (from the precondition } a \ge 0). \;\checkmark

Both conjuncts of I hold, so \{P\}\; q := 0;\, r := a \;\{I\}. Formally this is two applications of the assignment axiom composed by the sequence rule, but the substitution above is all the content. The precondition a \ge 0 is exactly what we needed to get 0 \le r off the ground — a first hint that preconditions are not decoration.

Step 2 — Maintenance

We must prove the body preserves the invariant when the guard holds: \{I \wedge r \ge b\}\; r := r - b;\; q := q + 1 \;\{I\}. Assume I and the guard r \ge b at the top. Write the new values as r' = r - b and q' = q + 1. Check both conjuncts of I for the primed values.

Conservation a = b\,q' + r': b\,q' + r' = b(q+1) + (r - b) = bq + b + r - b = bq + r = a, using a = bq + r from I. The added b and the subtracted b cancel exactly — that is why one peel of the remainder pairs with one bump of the quotient.
Non-negativity 0 \le r': we have r' = r - b, and the guard gives r \ge b, so r - b \ge 0. Here the guard r \ge b is doing the work — without it, subtracting b could drive r negative and break the invariant.

Both conjuncts of I hold of q', r', so the body restores I. Maintenance is discharged. (In pure Hoare logic you would derive the precondition of the composed body by two backward applications of the assignment axiom and then use the rule of consequence to show I \wedge r \ge b implies it — the algebra above is that consequence step.)

Step 3 — Exit implies the postcondition

By the while-rule, the loop establishes I \wedge \neg(\text{guard}), i.e.

\underbrace{a = b\,q + r \;\wedge\; 0 \le r}_{I} \;\wedge\; \underbrace{r < b}_{\neg(r \ge b)}.

Line this up against the postcondition Q:\; a = bq + r \wedge 0 \le r \wedge r < b: the first two conjuncts come straight from I, and the third, r < b, is exactly the negated guard handed to us at exit. So I \wedge \neg(r \ge b) \Rightarrow Q — in fact they are identical. The proof is complete: \{P\}\; \texttt{divide} \;\{Q\}, partial correctness established for every valid input at once.

Observe how the roles divided up. The invariant carried the conservation law a = bq + r and the lower bound 0 \le r through every iteration; the guard, on failing, supplied the upper bound r < b that the invariant alone never guaranteed. Invariant plus negated guard equals postcondition — the signature shape of every loop proof.

The state trace

Concretely, a = 17, b = 5. Watch the invariant 17 = 5q + r hold at every top-of-loop, and the loop halt the instant r < 5.

Point	q	r	5q + r	guard r \ge 5
before loop	0	17	17 ✓	true — iterate
after iter 1	1	12	17 ✓	true — iterate
after iter 2	2	7	17 ✓	true — iterate
after iter 3	3	2	17 ✓	false — exit

On exit q = 3, r = 2: indeed 17 = 5 \cdot 3 + 2 with 0 \le 2 < 5. The invariant column never changes — that is the conservation law made visible — and the guard flips to false exactly when the remainder has been squeezed below the divisor.

A second, shorter example: array sum

The same skeleton, run at speed. Specify \texttt{sum}(A) to return \sum_{j=0}^{n-1} A[j] for an array of length n.

function sum(A: readonly number[]): number { let s = 0; let i = 0; // invariant I: s === A[0] + ... + A[i-1] AND 0 <= i <= A.length while (i < A.length) { s = s + A[i]; i = i + 1; } // exit: i === A.length, so s === A[0] + ... + A[n-1] return s; }

Initialise: s = 0 is the empty sum \sum_{j=0}^{-1} with i = 0 — holds. Maintain: if s = \sum_{j=0}^{i-1} A[j], then after s := s + A[i] and i := i+1 we have s = \sum_{j=0}^{i} A[j] = \sum_{j=0}^{i'-1} A[j] — restored (the guard i < n guarantees A[i] is a valid element, keeping the bound i \le n). Conclude: the guard fails at i = n, and I then reads s = \sum_{j=0}^{n-1} A[j] — the postcondition. Same three boxes, same invariant-plus-negated-guard finish. Once you have seen the pattern twice, every loop proof is a fill-in- the-blanks exercise: state the invariant, initialise it, maintain it, and read the postcondition off I \wedge \neg b.

Every step above assumed the loop reaches exit — we proved "if it stops, r < b and the answer is right," and never that it stops. For divide it plainly does: each iteration strictly decreases r by b > 0 while keeping r \ge 0, and a non-negative integer cannot decrease forever. That quantity — the variant r, strictly decreasing in the well-founded order of the naturals — is the extra ingredient that upgrades partial correctness to total correctness. We deliberately keep the two apart because they use different tools (invariants and consequence for the "right answer," a well-founded variant for "terminates"); the termination argument gets its own treatment later.

Try to run the proof with a weaker precondition and it collapses. If b could be 0, the invariant's conservation clause a = bq + r becomes a = r forever, the guard r \ge 0 never fails (assuming a > 0), and the loop spins without end — the postcondition's r < b = 0 is unsatisfiable for r \ge 0, so no correct answer even exists. That is exactly why the precondition demands b > 0. Symmetrically, the maintenance step's non-negativity conjunct 0 \le r' was rescued only by the guard r \ge b; delete the guard's contribution and a subtraction could push r negative, violating I. A loop proof is a tightly-wound machine: the precondition seeds the invariant, the guard powers maintenance and delivers the final conjunct at exit. When a proof won't close, the culprit is almost always a precondition you under-stated or a guard fact you forgot to use.