A loop invariant is a property that remains true before and after every iteration of a loop.

A typical proof has three parts:

1. Initialization: the invariant is true before the first iteration.
2. Maintenance: if it is true before an iteration, the loop body preserves it.
3. Termination: when the loop ends, the invariant together with the exit condition implies the desired result.

For example, a search loop may maintain that any still-possible location of the target lies inside the current candidate interval.

A useful invariant is strong enough to imply the result at termination but simple enough to establish initially and preserve mechanically.

Loop invariants turn reasoning about changing program state into a reusable correctness technique for searching, sorting and iterative numerical algorithms.