Loop invariant

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 $S$:

• Initialisation — The initial claim $S_0$ must be true before the loop begins.
• Maintenance — If $S_{i-1}$ is true before iteration $i$ begins, then $S_i$ should be provably true after iteration $i$ is over (the inductive step).
  • i.e., given an assumed pre-condition, we must prove that the post-condition continues to hold.
• Termination — The final statement $S_k$ 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 $S$ 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 and CLRS chapter 2.