In computer science, loop invariants are proofs used to analyse the correctness of loop-based algorithms. We need to prove the following are correct, for a statement :
- Initialisation — The initial claim must be true before the loop begins.
- Maintenance — If is true before iteration begins, then will be true after iteration is over (the inductive step).
- Termination — The final statement implies the statement that we wish to justify is true.
i.e., a loop invariant is a variant of an induction proof where the “induction” stops because the loop terminates. When the first two properties hold, the invariant is true prior to every iteration of the loop.
We describe loop invariants as a predicate that must hold. These predicates should hold true throughout the loop’s execution, and essentially captures the main functionality of each loop. Statements usually involve the variables used and the intended outcome of the loop; we prove the three statements to prove correctness.
An example of this is given in the page about insertion sort.