Loop Invariant

Overview

A loop invariant $P$ is a condition that holds before, during, and after each iteration of a loop (e.g. for or while). These "timings" correspond to the three necessary properties of an invariant:

• Initialization
  • $P$ is true before the first iteration of the loop.
• Maintenance
  • If $P$ is true before an iteration, $P$ is also true before the next iteration.
• Termination
  • $P$ provides a condition used to prove an algorithm's correctness.

Notice loop invariants mirror mathematical induction. Initialization is analogous to an inductive base case while iteration is analogous to the inductive step.