A truth that survives every pass
A loop invariant is a statement about the program state that is true before the loop begins and remains true after each iteration. Proving the right invariant is the standard way to show an iterative algorithm is correct, playing the same role that induction plays for recursion.
Three parts to check
A loop invariant proof mirrors mathematical induction and has three obligations:
- Initialization: the invariant is true just before the first iteration.
- Maintenance: if it is true before an iteration, it is still true before the next one.
- Termination: when the loop ends, the invariant combined with the exit condition implies the desired result.
A worked sense of it
For insertion sort, a suitable invariant is that the subarray to the left of the current index is always sorted and contains the same elements it started with. Initialization holds because a single element is trivially sorted. Maintenance holds because each pass inserts the next element into its correct place. At termination the loop has passed every index, so the whole array is sorted, exactly the goal.
Key idea
A loop invariant is a property true before and after every iteration; proving its initialization, maintenance, and termination establishes that an iterative algorithm is correct, the iterative analogue of induction.