Induction and loop invariants: proving code correct for every n
Induction proves a claim for every n from a base case plus a step that carries truth from n to n+1; strong induction lets the step lean on all smaller cases. A loop invariant is the same proof in code: true before the loop, preserved by each pass, at exit yielding correctness.
Code review, Thursday afternoon. The diff is a tight little loop that batches user records for export, and the tests pass — for 3 records, for 10, for 100. The reviewer leaves one comment: “Why does this work for a million records? You tested three sizes.” The author types and deletes several replies. “It obviously generalizes” is not an argument; a million test cases will not fit in CI; and somewhere in everyone’s memory is the time pagination worked for every test fixture and then silently dropped one row per page in production — off by one, at scale, for six weeks. There is a way out of this corner, and it is the same trick mathematicians have used since the seventeenth century to make claims about infinitely many numbers without checking them one by one. The reviewer was not asking for more tests. They were asking for an invariant.
After this lesson you can state the two parts of an induction proof and explain why both are required, describe what strong induction adds, define a loop invariant and discharge the three proof obligations (initialization, maintenance, termination) on a simple loop.
Mathematical induction has two parts: a base case and an inductive step. How do you prove a statement about every natural number in finite time? Mathematical induction does exactly two things. Base case: show the claim holds for the first value, usually n = 0 or n = 1. Inductive step: show that if the claim holds for an arbitrary n (the induction hypothesis), then it holds for n + 1. Two finite proofs, infinite coverage. The standard picture: a row of dominoes. The base tips the first domino. The step guarantees each falling domino knocks over the next. Given both, every domino falls — including number one million, which nobody touched directly.
Both parts are load-bearing. Skip the base case and you can “prove” nonsense: the step “if n is even then n + 2 is even” is flawless, but starting from 1 it generates only odd numbers — a perfect chain of dominoes that nobody tipped. Skip the generality of the step and you get the classic broken proof that all horses are the same color: the argument quietly assumes two groups overlap, which fails exactly at n = 2 — one rung of the ladder is cracked, and everything above it falls down.
Strong induction lets the step use all smaller cases — natural fit for recursion. Sometimes “it worked for n” is not enough fuel for the step. Strong induction upgrades the hypothesis: assume the claim holds for all values up to n, then prove it for n + 1. This is the natural shape for recursion: a recursive function that handles its base case and is correct whenever its recursive calls on any smaller inputs are correct, is correct, full stop. Every time you trust mergeSort on the halves while writing the merge, you are reasoning by strong induction.
A loop invariant is induction in code: initialization, maintenance, termination. A loop invariant is a statement about the program’s variables that is true every time the loop checks its condition. Proving a loop correct with an invariant mirrors induction exactly: initialization (invariant holds before the first iteration — base case), maintenance (if it holds at the top of an iteration, it holds at the top of the next — inductive step), termination (the loop exits and at exit, invariant + loop-condition-false together imply the result you wanted). Three small checks and the function is correct for every input — including the empty array and the million-element array no fixture exercises.
Prove the running-sum loop correct with a loop invariant.
function sumFirst(nums) {
let total = 0;
let i = 0;
// INVARIANT: total === sum of nums[0..i-1] (the first i elements)
while (i < nums.length) {
total += nums[i];
i += 1;
// total now includes nums[i-1]: still the sum of the first i elements
}
return total;
}Initialization: before the loop, i = 0 and total = 0. The sum of zero elements is 0. Invariant holds.
Maintenance: assume the invariant holds at the top of an iteration — total is the sum of the first i elements. The body does total += nums[i] then i += 1, so total is now the sum of the first new i elements. Invariant preserved.
Termination: the loop exits when i === nums.length. At that point the invariant reads total === sum of nums[0..nums.length-1] — the sum of all elements. That is exactly what the function returns. Also, nums.length - i strictly decreases each pass, so exit is guaranteed.
Now spot the off-by-one bug: initialize i = 1 “because the first element is already in total.” Initialization check: total = 0, i = 1, but the sum of the first 1 element is nums[0] ≠ 0. The invariant fails before the loop even runs — the proof points at the bug immediately.
▸Why this works
Why does this argument pattern get to call itself proof while “it worked in staging” does not? Because induction is just dressed-up modus ponens, the valid form from the previous unit. The step proves a universal conditional — for every n, P(n) → P(n+1) — and the base supplies P(0). Apply modus ponens once: P(1). Again: P(2). For any target n the chain is a finite, fully valid deduction. Testing, by contrast, establishes P at scattered points with no conditional connecting them — which is why three passing sizes say nothing about the fourth.
An induction proof shows P(0) and P(n) → P(n+1). Is P(1000000) proven? Type yes or no.
What happens if you skip the base case in an induction proof?
Name the three obligations for a loop invariant proof.
What is the loop invariant for 'sum the first i elements in total'?
If the initialization check fails, where is the bug?
What exactly must you establish about a loop invariant to conclude the loop produces the right answer?
Mathematical induction proves a claim about every natural number with two finite pieces: a base case (the claim holds at n = 0) and an inductive step (if it holds at an arbitrary n, it holds at n + 1), after which any specific n is reached by a finite chain of modus ponens. Both pieces are mandatory: a perfect step with no base is an untipped domino row, and a step proved only for examples is the all-horses fallacy with its crack hidden at one rung. Strong induction strengthens the hypothesis to all values up to n — equivalent in power, but the natural fit for problems that split into arbitrarily smaller parts: prime factorization, merge sort, and every recursive function that is correct whenever its recursive calls on smaller inputs are. A loop invariant transplants the proof into code: state what the variables mean at every condition check, then discharge initialization (true before the loop; base case), maintenance (each iteration preserves it; inductive step), and termination (a strictly decreasing quantity forces exit, where invariant plus failed loop condition imply the answer). The payoff over testing is categorical: the proof covers every input, and when a proof obligation fails it points at the guilty line — initialize the index at 1 in the sum loop and initialization itself refuses, exposing the off-by-one before the loop runs. Write the invariant as a comment; ship the reason, not just the code.
Practice
Start at the top. Tasks go easiest → hardest: recall a fact, apply it to a case, then a senior-level stretch. Open one, attempt it, then reveal.
Something unclear?
Ask a question about this lesson. Questions are anonymous and go straight to the author to make the lesson better.