Algorithmic Foundations
Correctness & Invariants
An invariant is a property that stays true across every iteration of a loop or every level of a recursion. Proving an algorithm correct almost always means finding the right invariant and showing it holds at the start, is preserved by each step, and implies the answer at the end.
- A loop invariant must hold: (1) before the first iteration, (2) if true before an iteration then true after it, (3) at termination in a form that implies correctness
- This is induction in disguise — the invariant is the inductive hypothesis, the loop step is the inductive step
- Termination must be argued separately from correctness: a variant (a value that strictly decreases and is bounded) proves the loop ends
- Off-by-one bugs are almost always an invariant that was never stated precisely — "sorted up to index i" vs "sorted up to and including index i" are different invariants
- Recursive correctness proofs mirror loop invariants: base case = initialization, recursive case = preservation, assuming smaller instances are already correct
The classic example is insertion sort: the invariant is "at the start of each outer-loop iteration, a[0..i-1] is sorted." Initialization is trivial (a single element is sorted). Preservation is the inner loop: it inserts a[i] into the correct position among a[0..i-1], restoring the invariant for i+1. Termination: when i reaches a.length, the invariant says a[0..n-1] is sorted — exactly the goal. This is the entire correctness proof, and it is also exactly how you would explain the algorithm to a colleague.
static void insertionSort(int[] a) {
for (int i = 1; i < a.length; i++) {
// invariant: a[0..i-1] is sorted
int key = a[i];
int j = i - 1;
while (j >= 0 && a[j] > key) {
a[j + 1] = a[j];
j--;
}
a[j + 1] = key;
// invariant restored: a[0..i] is sorted
}
// loop exit: i == a.length, so a[0..n-1] is sorted
}| Step | Question answered | Insertion-sort example |
|---|---|---|
| Initialization | Is it true before the first iteration? | a[0..0] (one element) is trivially sorted |
| Maintenance | If true before an iteration, is it true after? | Inner loop inserts a[i] into its sorted position |
| Termination | Does it imply correctness when the loop ends? | i = n ⟹ a[0..n-1] sorted ⟹ done |