Proving a Loop Works
Testing shows the presence of bugs; reasoning can show their absence. The central tool for arguing an iterative algorithm is correct is the loop invariant: a property that is true before the loop starts and remains true after every iteration.
A loop-invariant argument has three parts, mirroring induction:
| Phase | Requirement |
|---|---|
| Initialization | The invariant is true before the first iteration. |
| Maintenance | If true before an iteration, it is still true after. |
| Termination | The loop ends, and the invariant implies the result. |
In Action and Pitfalls
Consider summing a list with a running total. The loop invariant is "total equals the sum of the elements processed so far." It holds initially (0 elements), is maintained as each step adds the next element, and at termination gives the sum of all elements.
This reasoning catches off-by-one and boundary bugs that testing misses.
Common pitfall: Confusing "the loop ran without crashing" with "the loop is correct." Only a well-chosen invariant, shown to hold at initialization and through every iteration, establishes true correctness.