= Loop invariant
{wiki}
A statement true whenever execution reaches a chosen point in a loop, usually immediately before its condition is tested. Establish it initially, preserve it through each iteration, and combine it with the exit condition to establish <algorithm correctness>. Termination needs a separate argument.<CS 2112 Fall 2019/Loop invariants>[CS 2112 Fall 2019; Loop invariants, Using loop invariants to show code is correct: the three partial-correctness obligations and separate Termination step]{ref}
Write $I$ for the <loop invariant>, $B$ for the condition, $P$ for the <precondition>, and $Q$ for the <postcondition>. Prove that initialization under $P$ establishes $I$, that a completed body starting with $I$ and $B$ restores $I$, and that $I$ with false $B$ implies $Q$.<CS 2112 Fall 2019/Loop invariants>[CS 2112 Fall 2019; Loop invariants, Using loop invariants to show code is correct: Establishment, Preservation, and Postcondition]{ref}
In the <prefix maximum correctness example>, the <loop invariant> remembers exactly the <maximum> of the processed prefix and the valid index bounds. The weaker statement $\mathrm{best}\geq a_0$ survives every iteration, but does not imply the <postcondition>: for $[3,1,4,4,2]$, the wrong value $3$ satisfies it. A useful <loop invariant> retains enough information to recover the answer when the condition becomes false.
Back to article page
