3 · Correctness: loop invariants, pre/postconditions
Loop invariants: initialization, maintenance, termination.
In one sentence
To prove an algorithm is correct, show that it gives the right answer whenever it stops (partial correctness) and that it always stops (termination). For loops, the tool is a loop invariant; for recursion, it's induction.
Everyday analogy
A running receipt at a shop. While items are scanned, the screen always shows "the total of everything scanned so far". That sentence is true:
- before the first item (total = 0 for zero items): initialization,
- after every scan, if it was true before: maintenance,
- and when the last item is scanned, it tells you exactly what you owe: termination.
That sentence is a loop invariant.
Key rules
| Part of a loop-invariant proof | What you show |
|---|---|
| Initialization | The invariant is true before the first iteration |
| Maintenance | If it's true before an iteration, it's still true before the next one |
| Termination | When the loop stops, invariant + exit condition ⇒ the output is correct |
| Other tools | Use for |
|---|---|
| Induction | recursive algorithms (base case = smallest input; step = trust the recursive call) |
| Pre/postconditions | the "contract": if the input satisfies the precondition, then the output satisfies the postcondition |
Finding an invariant
Ask: "After rounds, what is true about the part of the input already processed?"
Write the invariant in terms of the loop variable (i) and the processed part (A[1..i-1]).
Algorithm (our own example):
Power(x, n) // precondition: n ≥ 0
1 p ← 1
2 for i ← 1 to n do
3 p ← p · x
4 return p // postcondition: p = xⁿInvariant: at the start of the iteration with loop variable , .
Trace with , :
| Moment | Invariant holds? | |||
|---|---|---|---|---|
| before 1st iteration | 1 | 1 | ✅ initialization | |
| before 2nd | 2 | 3 | ✅ maintenance | |
| before 3rd | 3 | 9 | ✅ | |
| before 4th | 4 | 27 | ✅ | |
| loop exits | 5 | 81 | ✅ termination ⇒ |
Common mistakes
- Invariant written about the whole array instead of the processed part
A[1..i-1]. - Off-by-one: mixing "start of iteration" and "end of iteration". Pick one and stay consistent.
- Skipping termination, or not substituting the exit value of .
- Forgetting to argue that the loop actually stops.
Mastery check
Solve without hints
LinearSearch(A, n, key): for i ← 1 to n: if A[i] = key then return i, then return NIL.
State a loop invariant and prove that if it returns NIL, the key is not in the array.
Invariant: at the start of iteration , no element of equals key. Init: is empty ✓. Maintenance: if we don't return at , then key, so has no key ✓. Termination: if the loop finishes, , so no element of equals key, and returning NIL is correct ∎
Status
Tick all six steps to unlock “Mastered”.
Which study mode worked for you?
References
- 04 Correctness & Space: Slide 10 (partial correctness + termination), 11–15 (loop invariants, arrayMax case study), 16 (Sum-Array task), 17 (induction), 18–19 (pre/postconditions).
- CLRS 4e §2.1 (loop invariants and the correctness of insertion sort).