Loop Invariants

A loop invariant is a logical statement that holds whenever control reaches a designated point in a loop, usually immediately before the condition is tested. It describes the relationship between the processed state, the unprocessed state, and the intended result.

The invariant need not remain true after every individual statement inside the body. The body may temporarily violate it, provided the statement is restored before the next iteration boundary.

The initialization proof shows that the invariant holds before the first iteration. For a loop that has processed the prefix A[0..i), initialization often uses i = 0; the empty prefix satisfies the claimed property.

This step exposes off-by-one errors early. If the invariant describes an inclusive range but the code initializes an exclusive boundary, the proof and implementation disagree before the loop starts.

The maintenance proof assumes the invariant and loop condition hold at the start of an iteration. It then shows that executing the body re-establishes the invariant for the updated state.

This is an induction step over iteration count. The proof must account for every mutation used by the invariant, including index changes, swaps, accumulator updates, and data-structure operations.

When the loop exits, the invariant still holds and the loop condition is false. Combining those facts should imply the required postcondition. An invariant that remains true but says too little at exit cannot establish correctness.

For a scan with invariant “the first i elements have been processed,” termination at i = n turns the prefix property into a property of the complete input.

Initialization, maintenance, and the exit argument establish partial correctness: if the loop terminates, its result satisfies the postcondition. They do not by themselves prove that termination occurs.

Total correctness adds a variant, or ranking function, that decreases on every iteration and cannot decrease indefinitely. A non-negative integer such as right − left commonly serves this role.

Insertion sort maintains that the prefix A[0..i) contains the original first i elements in sorted order. The invariant holds initially for the one-element prefix.

The body inserts A[i] into that sorted prefix by shifting larger elements right. The resulting prefix A[0..i+1) is sorted and contains the same elements. At i = n, the complete array is sorted.

A binary-search invariant can state that if the target exists, it lies inside the current half-open interval [lo, hi). Comparing the midpoint discards only a region that cannot contain the target.

Maintenance depends on matching comparisons with boundary updates. The interval length hi − lo strictly decreases, proving termination. At an empty interval, the invariant implies that the target is absent.

Two-pointer algorithms usually maintain facts about regions outside two moving boundaries. During partitioning, one invariant may state that every value before left satisfies a predicate and every value after right does not.

Each iteration classifies at least one unprocessed element and moves a boundary. Correctness follows when the unclassified interval becomes empty. The invariant must state both the region property and the region boundaries.

Nested loops need an invariant at each level. The inner loop is proved relative to the state fixed by one outer iteration. Its postcondition then supplies the fact needed to maintain the outer invariant.

For matrix multiplication, the inner loop can maintain a partial dot product, while the outer loops maintain which output cells are complete. Treating all indices in one assertion often obscures which body is responsible for each fact.

Start from the postcondition and weaken it just enough to describe partial progress. Replace “the entire array is sorted” with “the prefix before i is sorted,” or replace a complete sum with a sum over the processed range.

Then choose loop state that makes the claim maintainable. Boundary conventions such as half-open intervals reduce special cases because empty and complete ranges share the same representation.

An invariant can be true yet useless, such as i ≥ 0 when the proof needs a relationship between i and the data. It can also be too strong to initialize or preserve.

Other failures include proving maintenance without the loop condition, omitting multiset preservation during sorting, and assuming termination from a bounded variable that does not change monotonically. Each proof obligation checks a different defect.

Runtime assertions can encode executable parts of an invariant and detect violations during tests. They provide evidence for observed executions, not a proof over every input.

Static verification systems express preconditions, postconditions, invariants, and termination measures as proof obligations. Hoare logic writes a command between assertions as {P} C {Q}; the loop rule uses an invariant to connect repeated executions of the body.

A loop invariant states what is preserved at an iteration boundary. Correctness requires proving initialization, maintenance, and that the invariant plus loop exit implies the postcondition.

A separate decreasing variant establishes termination. Concrete invariants for sorted prefixes, shrinking search intervals, classified regions, and partial sums turn loop behavior into induction over iterations.