Recipe
Check whether a loop is totally correct
Use when: you're given a loop and asked whether it terminates, whether its output is correct, or both
Goal: a verdict on termination, a verdict on correctness, and the variant or counterexample that backs each one up
Taught in Correctness and termination
Quick recipe
-
1
Identify a quantity that changes every iteration of the loop and is bounded below by some fixed value the loop cannot pass.
Example
For
while n > 0: n = n - 1, the quantity n changes every pass and can never go below 0 once the loop starts with n \geq 0.Why: a variant is the tool a termination proof is built on, so naming one is always the first move.
-
2
Check both properties directly: the quantity must go down by at least a fixed amount every iteration, and it must have a floor it cannot cross.
Example
n decreases by exactly 1 each pass, a strict decrease, and cannot fall below 0, a genuine bound, so the loop terminates.
- the quantity strictly decreases every iteration and is bounded below — the loop terminates; continue to Step 3.
- the quantity does not strictly decrease every iteration, or has no lower bound — termination is not proved; look for a different variant, or check whether the loop can run forever.
Why: a quantity that could decrease forever with no floor, or that sometimes stays the same, does not actually force the loop to stop.
-
3
Pick a short, specific input and run the loop by hand, step by step, recording every variable's value each iteration.
Example
Take
for i = 0 to n-1: if A[i] > A[0]: A[0] = A[i], meant to find the maximum. Trace it on A=[5,2,9]: at i=0, A[0]=5 compares to itself. At i=1, 2>5 is false. At i=2, 9>5 is true, so A[0] becomes 9.Why: a trace turns "I think it's right" into a checked claim on at least one real input.
-
4
Think about which input pattern the trace above did not cover, then check whether that pattern breaks the loop.
Example
The comparison above is always against the current A[0], not the original one. So a later entry that beats an earlier update, but not the true original maximum, can slip through in a longer array.
- no input breaks the loop — the correctness argument holds so far, but only a loop invariant proof, coming next section, makes it certain for every input.
- some input produces a wrong output — the loop is not correct; report the counterexample, not just a passing trace.
Why: one successful trace never proves correctness for every input; only a genuine invariant argument or a discovered counterexample settles it.
Common mistakes
- Treating one successful trace as proof of correctness for every possible input.
- Picking a variant that can decrease by a different amount each time without checking that it never stops decreasing.
- Confusing "the loop always runs a fixed number of times" with "the loop is correct."
- Forgetting to check that the variant has a genuine lower bound, not just that it decreases.