1
Initialisation is the base case
The invariant must hold before any iteration has run, which is usually immediate and is usually where an off-by-one hides.
Lesson · Induction and Recursion · Correctness
Loop Invariants and Program Correctness
A loop invariant is a statement true before the loop and preserved by every iteration. Together with termination it proves the loop computes what it should — and the argument is exactly induction.
INITIALISATION the invariant holds before the first iteration
MAINTENANCE if it holds before an iteration, it holds after
TERMINATION the loop stops, and the invariant then gives the result
This is induction: base case, step, conclusion.
Three obligations
Core ideas
What this lesson establishes
The three parts of a loop-invariant proof are the three parts of an induction proof, renamed.
2
Maintenance is the inductive step
Assume the invariant before an iteration and prove it after. The loop body is what you reason about.
3
Termination converts the invariant into the result
The invariant plus the negated loop condition should give exactly the postcondition. If it does not, the invariant is too weak.
The material
Loop invariants
The method, three worked loops, and how to find an invariant.
Definition · Loop invariant
A loop invariant is a statement that is true immediately before the loop begins and remains true immediately before each subsequent iteration.
Summing an array
SUM(A): invariant: s = A[0] + … + A[i−1]
s = 0
i = 0
while i < n:
s = s + A[i]
i = i + 1
return s
Initialisation. Before the loop, i = 0 and s = 0; the sum of the first zero elements is 0, so the invariant holds vacuously.
Maintenance. Suppose s = A[0] + ⋯ + A[i−1] at the top of an iteration. The body adds A[i] to s and increments i, so afterwards s = A[0] + ⋯ + A[i−1] with the new i — the invariant again.
Termination. The loop exits with i = n, and the invariant then reads s = A[0] + ⋯ + A[n−1], which is the whole sum. That the loop exits follows because i increases by 1 each iteration and is bounded above by n.
Insertion sort
for j = 1 to n−1:
key = A[j]
i = j − 1
while i ≥ 0 and A[i] > key:
A[i+1] = A[i]
i = i − 1
A[i+1] = key
invariant (outer loop): A[0..j−1] contains the original first j
elements, in sorted order
Initialisation: at j = 1 the subarray A[0..0] is one element, trivially sorted. Maintenance: the inner loop shifts elements greater than key one place right and inserts key in the gap, so A[0..j] ends sorted and holds the same elements. Termination: the outer loop ends with j = n, so A[0..n−1] is sorted — which is the postcondition.
The invariant says two things: sorted, and the same elements. Dropping the second half would leave the proof compatible with an algorithm that sorts by replacing the array with zeros. Invariants that are too weak are the usual failure, and they fail at the termination step.
Finding an invariant
- Start from the postcondition. What should be true at the end? The invariant is usually that statement with the loop variable in place of its final value.
- Include everything the proof needs. "Sorted" alone is not enough; "sorted and a permutation of the original" is.
- Check the boundaries. The invariant must hold when the loop has run zero times, which is where the vacuous cases live.
Theorem · Partial and total correctness
Partial correctness is: if the loop terminates, the postcondition holds. Total correctness adds that it does terminate. An invariant gives the first; a decreasing bounded quantity gives the second.
The distinction matters. A loop with a correct invariant that never exits is partially correct and useless. Termination is proved the same way as for a recursion: exhibit a quantity that strictly decreases and cannot decrease forever.
Interactive
Algorithms and growth
Counts from running, not from quoting
Method
Proving a loop correct
State the invariant before writing anything else.
1
Write the postcondition
What must be true when the loop finishes. Without it there is nothing to aim the invariant at.
2
Guess an invariant and test the boundaries
Usually the postcondition with the loop variable substituted. Check it holds before any iteration has run.
3
Prove maintenance
Assume the invariant at the top of an iteration, follow the body, and show it holds at the top of the next.
4
Prove termination and combine
A decreasing bounded quantity ends the loop; the invariant plus the negated loop condition must give the postcondition. If it does not, strengthen the invariant.
Invariants
Score 0 / 0Choose the answer you can justify.
Euclid's algorithm
“The Euclidean Algorithm” in Number Theory and Cryptography uses this; here it is the correctness argument.
GCD(a, b):
while b ≠ 0:
(a, b) = (b, a mod b)
return a
INVARIANT gcd(a, b) = gcd(a₀, b₀) for the original inputs
INITIALISATION trivially true before the first iteration.
MAINTENANCE gcd(a, b) = gcd(b, a mod b) — any common divisor of
a and b divides a − qb, and conversely. So the pair
changes but its gcd does not.
TERMINATION b strictly decreases and is a non-negative integer,
so the loop ends, with b = 0. Then
gcd(a, 0) = a, and by the invariant that equals
gcd(a₀, b₀). ∎
The invariant is the entire proof: the algorithm works because the quantity it is computing never changes while the numbers get smaller. Every good invariant has that character — it names what the loop preserves, which is more informative than what the loop does.
Common mistakes
1
An invariant too weak to give the postconditionTest it at termination before doing any other work: substitute the exit condition and see whether the postcondition follows.
2
Checking maintenance and skipping initialisationThe base case is where off-by-one errors live, and it is one line to check.
3
Proving partial correctness and calling it doneTermination is the other half. A quantity that strictly decreases and is bounded below is all it takes to write.
Check your understanding
✓
Finish when you can state an invariant strong enough to close the argument.
Write a loop computing xⁿ by repeated multiplication and state its invariant. Then check that at exit the invariant plus the loop condition gives exactly result = xⁿ — if it needs an extra sentence, the invariant was too weak.
Note: This is the whole of Hoare logic in miniature: preconditions, postconditions and invariants, with a proof rule for each construct. “Correctness and Termination” in Algorithms and Complexity returns to correctness as a property to be established before efficiency is worth measuring.