Loop Invariants and Correctness Proofs

A loop invariant is a logical assertion about the variables of a program — an equation, an inequality, a claim about which elements are sorted, a claim about which set has been visited — that is designed to be true immediately before the loop's test is evaluated, on every pass through the loop, including the very first and the very last. It is not a claim about what the whole algorithm computes; it is a claim about a snapshot of memory at a specific point that recurs over and over as the loop runs. The reason invariants are useful is that a loop is really a compressed, repeated instruction, and repetition is exactly what induction is built to handle. In an inductive proof over the natural numbers, you prove a base case and an inductive step ("if true for $k$, then true for $k+1$"), and conclude the statement holds for all $n$. A loop invariant proof does the same thing, indexed not by an abstract integer but by the iteration count of the loop:

• Initialization. The invariant is true before the first iteration begins. This is the base case.
• Maintenance. If the invariant is true before an iteration, it remains true before the next iteration. This is the inductive step; here the loop body is analyzed line by line.
• Termination. When the loop exits — because its guard condition becomes false — the invariant, combined with the reason the loop stopped, implies a useful fact: usually, that the algorithm has done what it claims to do.

Note the asymmetry with plain induction: ordinary induction proves a statement for infinitely many values of $n$. A loop invariant argument is used for a finite, bounded process, so the interesting content at termination is not "for all $n$" but "for the specific $n$ at which the loop stopped, look at what the invariant tells us." This is why termination is listed as a separate, distinct obligation, rather than folded into maintenance: you must also argue that the loop terminates at all (usually via a bound that strictly decreases, or an index that strictly increases toward a limit), and then translate the invariant-at-exit into the postcondition you promised the caller. Finally, a subtlety that trips up many first attempts: the invariant must be strong enough to be useful at termination but provable at every step. A trivially true statement (like "the array has a length") satisfies initialization and maintenance vacuously but tells you nothing when the loop ends. Conversely, an overly strong claim (like "the array is fully sorted" stated too early) may be false mid-loop and thus fail maintenance. Choosing the right invariant is the central design skill; this article's job is to show how that choice is made and checked.

We illustrate the method on insertion sort, chosen because its invariant is the cleanest possible instance of the technique, then apply the same three-part discipline to a second algorithm to show the pattern is general. The algorithm sorts an array $A[1..n]$ in place. On iteration $j$, it takes the element $A[j]$ and inserts it into its correct position among the already-sorted prefix $A[1..j-1]$. ``` INSERTION-SORT(A, n): for j = 2 to n: key = A[j] // Insert A[j] into the sorted sequence A[1..j-1] i = j - 1 while i >= 1 and A[i] > key: A[i + 1] = A[i] i = i - 1 A[i + 1] = key ```

Choosing the invariant. We claim, for the outer `for` loop: > Invariant: At the start of each iteration of the `for` loop (indexed by `j`), the subarray `A[1..j-1]` consists of the elements originally in `A[1..j-1]`, but in sorted order. This is exactly the kind of statement we want: strong enough to be useful (when the loop ends, it will tell us the whole array is sorted), yet checkable at each step.

Initialization. Before the first iteration, $j = 2$, so the claim is about `A[1..1]`, a single element. A one-element subarray is trivially sorted, and it certainly contains "the elements originally there" since nothing has moved yet. The base case holds.

Maintenance. Assume the invariant holds at the start of iteration $j$: `A[1..j-1]` is the original elements of that range, sorted. The loop body removes `A[j]` into `key`, then shifts elements of `A[1..j-1]` that are greater than `key` one position to the right, and finally places `key` into the gap that shifting created. Because `A[1..j-1]` was sorted before this body ran, the shifting process finds exactly the correct insertion point — it stops (`i` decrements) exactly when it meets an element `A[i] <= key` or falls off the front of the array. After insertion, `A[1..j]` contains the same multiset of elements as `A[1..j]` did before (nothing was created or destroyed, only moved and one value re-inserted) and is now sorted. So at the start of iteration $j+1$, the invariant holds for `A[1..j]` — which is precisely the invariant statement with $j$ replaced by $j+1$. The inductive step is verified.

Termination. The `for` loop's counter `j` increases from 2 and the loop exits when `j` exceeds `n`, i.e., after the iteration for $j = n$ completes. Plugging $j = n+1$ into the invariant: `A[1..n]` — the entire array — is the original elements of `A[1..n]` in sorted order. That is exactly the specification of sorting. The proof is complete. Observe how termination did real work here: it is the step where "the invariant holds for `A[1..j-1]` on every iteration" becomes "therefore the entire array is sorted," by noting the specific value of $j$ at which the guard condition fails.

The inner loop, too

A full proof should also justify the inner `while` loop, since it is where the actual data movement — and the actual risk of an off-by-one bug — lives. > Inner invariant: At the start of each iteration of the `while` loop, the subarray `A[i+1 .. j]` consists of the elements that originally occupied `A[i .. j-1]`, and every element in it is strictly greater than `key`. Initialization: before the loop starts, $i = j-1$, so `A[i+1..j]` is just `A[j..j]`, a single-element (possibly empty in the sense of holding just the shifted-out slot) range; vacuously the claim holds since there is nothing yet to check against `key` (this is the boundary case worth being careful about in an exam-quality proof). Maintenance: each iteration checks `A[i] > key`; if true, it moves `A[i]` one slot right (into `A[i+1]`) and decrements `i`. This preserves the claim: the shifted range grows by exactly the element that was just found to be `> key`. Termination: the loop stops either because `i < 1` (we reached the front of the array) or because `A[i] <= key`. In either case, `A[i+1]` is the correct empty slot for `key` — every element strictly greater than `key` has been pushed one to the right, and either we are at the array boundary or the element now at position `i` is `<= key`. Writing `key` into `A[i+1]` therefore restores full sorted order of `A[1..j]`. This inner-loop termination fact is exactly what the outer maintenance step above relied on. ``` PSEUDOCODE — template for any invariant proof State the invariant I(k), a property indexed by the iteration counter k, true "at the top" of iteration k (before the loop guard is tested). 1. INITIALIZATION: Show I(k0) holds, where k0 is the value of the counter before the first test of the loop guard. 2. MAINTENANCE: Assume I(k) holds and the loop guard is true (so the body runs). Trace the body's effect on the state. Show I(k+1) holds afterward (i.e., before the next guard test). 3. TERMINATION: Identify the value k at which the loop guard first fails. Combine I(k) with "guard is false at k*" to derive the desired postcondition. (Separately: argue the loop guard DOES eventually become false — e.g. a counter is bounded and strictly monotonic — otherwise the algorithm just doesn't terminate and step 3 is vacuous.) ```

Strictly speaking, "complexity" here refers to two separate things: the running time of the algorithm being proved correct, and the size/cost of the correctness proof itself. Both are worth being precise about.

Running time of insertion sort. The outer loop runs $n-1$ times. In iteration $j$, the inner `while` loop runs at most $j - 1$ times (it can only move through the sorted prefix). In the worst case (reverse-sorted input), this gives

In the best case (already sorted input), the inner loop's condition `A[i] > key` fails immediately every time, giving $\Theta(n)$. This is unrelated to the invariant proof itself — the proof establishes correctness for all inputs, while the running time bound requires a separate counting argument, exactly the kind covered by Analyzing Loops by Counting Operations. It is worth stressing: an invariant proof says nothing about how fast the algorithm is; a separate operation count is needed for that, and the two analyses are complementary, not substitutes for each other.

Cost of the proof. The invariant technique itself has no "running cost" — it is a static, one-time mathematical argument performed on the algorithm's text, done once regardless of $n$. This is one of its main appeals: a single finite proof certifies correctness for every array size and every input ordering simultaneously, which testing can never do (testing all inputs is usually infeasible, and even feasible test suites cannot rule out an input nobody thought to write down).

Correctness argument, restated as induction. Formally, let $P(k)$ be the invariant statement evaluated with the loop counter equal to $k$. The three parts show:

By ordinary mathematical induction, $P(k)$ holds for every $k$ the loop counter actually reaches. Since the loop is guaranteed to terminate — insertion sort's outer counter `j` strictly increases and is bounded above by $n$, so it must eventually exceed $n$ — there is a final value $k^*$ at which the guard first fails. $P(k^*)$, plus the negated guard, together imply the postcondition (Termination). This is exactly why the method is airtight: it is induction, and induction is valid for any well-ordered index set, which the iteration counter always is because loops (as opposed to unbounded recursion or non-terminating processes) are only useful algorithms if they halt.

Honesty about tradeoffs. The invariant method proves partial correctness — "if the loop terminates, the output is correct" — plus, separately, termination, together giving total correctness. It says nothing about efficiency, numerical stability, or behavior under concurrent modification of shared state; those require separate arguments (complexity analysis, floating-point error analysis, and race-condition reasoning respectively). It also gives no help in discovering the right invariant — that remains a creative step, usually guided by restating the postcondition and asking "what partial version of this is already true after $k$ steps?"

We trace `INSERTION-SORT` on the concrete array $A = [5, 2, 4, 6, 1, 3]$ ($n = 6$), checking the outer-loop invariant at the top of every iteration.

Reading one row in detail, $j = 5$ (inserting `key = A[5] = 1`): entering this iteration the invariant guarantees `A[1..4] = [2, 4, 5, 6]` is sorted. The inner loop compares `key = 1` against `6, 5, 4, 2` in turn — all are greater than `1`, so all four shift right, `i` walks down to `0`, and the loop stops because `i < 1`. We write `key` into `A[1]`. The result, `A[1..5] = [1, 2, 4, 5, 6]`, matches the invariant's promise for $j = 6$: exactly the elements originally in `A[1..5]`, now sorted. Nothing here depended on the specific numbers — the same argument works verbatim for any values, which is the entire point of proving it once rather than testing it repeatedly. At $j = 7$ the outer guard `j <= n` (i.e. `7 <= 6`) is false, so the loop exits, and the invariant — now instantiated at `A[1..6]`, the whole array — delivers exactly the postcondition "the array is sorted," matching the final row of the table.

A second, less symmetric example: linear search

To show the method is not special to sorting, consider linear search for a target `v` in `A[1..n]`, returning the first matching index or a sentinel: ``` LINEAR-SEARCH(A, n, v): i = 1 while i <= n and A[i] != v: i = i + 1 if i <= n: return i else: return NOT-FOUND ```

Invariant: at the start of each iteration (value `i`), none of `A[1], ..., A[i-1]` equals `v`. Initialization: at `i = 1`, the claim is about the empty range `A[1..0]` — vacuously true. Maintenance: if the loop body runs, the guard was true, meaning in particular `A[i] != v`. Combined with the invariant (`A[1..i-1]` has no match), we get `A[1..i]` has no match — exactly the invariant for the incremented counter `i+1`. Termination: the loop can end two ways. If it ends because `i > n`, the invariant says `A[1..n]` has no match, correctly justifying `NOT-FOUND`. If it ends because `A[i] == v` (while `i <= n`), the invariant says `A[1..i-1]` has no match, so `i` is genuinely the first occurrence — correctly justifying `return i`. Notice the invariant alone is not enough at termination; you must also case-split on which part of the compound guard failed, a detail routinely missed by students proving loops with `and`/`or` conditions.

The loop invariant as a formal proof device grew out of the broader program of program verification: treating a piece of code the way mathematicians treat a theorem, with axioms, preconditions, postconditions, and a calculus for deriving one from another. This effort matured in the late 1960s, converting decades of informal "this loop obviously works" folklore into a rigorous discipline that could, in principle, be checked mechanically.

Hoare's 1969 paper "An Axiomatic Basis for Computer Programming" introduced what is now called Hoare logic, built around triples $\{P\} \, S \, \{Q\}$ meaning "if precondition $P$ holds and statement $S$ executes, postcondition $Q$ holds afterward." The rule for `while` loops in that system is precisely the loop invariant: if $\{I \land B\} \, S \, \{I\}$ (the invariant $I$ is preserved by the body $S$ whenever the guard $B$ holds), then $\{I\} \; \texttt{while } B \texttt{ do } S \; \{I \land \lnot B\}$ — the invariant conjoined with the negated guard, exactly what the "termination" step of this article exploits. Around the same period, Robert Floyd's 1967 paper "Assigning Meanings to Programs" had already introduced the closely related idea of associating assertions with points in a flowchart and verifying that execution preserves them — flowchart assertions are the direct ancestor of the loop invariant, and Floyd's method for proving termination via a decreasing well-founded quantity (the "variant") is exactly the missing piece warned about above.

Loop invariants are not merely a classroom exercise; they are the intellectual backbone of how correctness claims about iterative code are actually justified in serious software engineering. Formal verification tools — model checkers, deductive verifiers such as Dafny, and static analyzers built on Hoare logic — require the programmer (or an automated inference engine) to supply loop invariants before they can certify a program; without one, the tool cannot reason past the first iteration of any loop. This matters acutely in safety-critical domains: avionics software, medical device firmware, and railway signaling systems are often required, by certification standards, to carry machine-checked proofs, and every `while` and `for` loop in such code needs an invariant on file. In everyday algorithm design, the invariant is how textbook algorithms — binary search, the partitioning step of Quicksort, Dijkstra's shortest-path relaxation, the greedy exchange arguments behind Huffman coding and minimum spanning trees — are certified correct rather than merely "observed to work on examples." Binary search's invariant ("the target, if present, lies within the current `[lo, hi]` window") is the standard explanation for why the classic implementation bug (`mid = (lo + hi) / 2` overflowing, or an off-by-one in updating `lo`/`hi`) breaks correctness: it is precisely a violation of maintenance. Compiler writers use invariant-style reasoning to justify loop transformations (unrolling, fusion, strength reduction) are semantics-preserving, since an optimization is safe exactly when it does not disturb the invariant the original loop maintained. And database query planners rely on invariant arguments to prove that iterative join and aggregation algorithms produce results consistent with the relational algebra they are meant to implement. Beyond software, the invariant-and-induction pattern is the same reasoning skeleton used to prove correctness of recursive algorithms (each recursive call plays the role of "the next iteration"), which is exactly the natural next topic once loop invariants feel comfortable: Correctness of Recursive Algorithms by Induction. It also connects tightly with Mathematical Induction as the underlying logical principle, and with Analyzing Loops by Counting Operations as the complementary tool needed once correctness, rather than speed, is no longer the open question.

Ask the tutor: Can you show me how to construct a loop invariant for a binary search implementation and use it to explain the classic off-by-one bug?