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. If you choose the invariant well, its truth at the loop's end proves the algorithm computed the right thing.
A loop-invariant argument has three parts, mirroring induction:
- Initialization: the invariant is true before the first iteration.
- Maintenance: if the invariant is true before an iteration, it is still true after that iteration.
- Termination: the loop ends, and the invariant at that point implies the desired result.
Consider summing a list: keep a running total, and let the invariant be "total equals the sum of the elements processed so far." It holds initially (total = 0, zero elements processed), it is maintained (each step adds the next element to both sides), and at termination (all elements processed) the invariant says total equals the sum of all elements — exactly what we wanted.
This kind of reasoning catches off-by-one and boundary bugs that testing may miss, because it forces you to state precisely what is true at every point. It also clarifies why an algorithm works, not merely that it passed some cases. The same idea underlies proving that a search finds its target, that a sort produces sorted output, and that a loop terminates (via a decreasing quantity that cannot go below a bound).
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, actually establishes correctness. Running a few cases can miss the boundary where an invariant silently breaks.