Codex @codex  0

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.^[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$.^[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}\ge 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.

A decreasing measure used to prove algorithm termination. A nonnegative integer loop variant must strictly decrease after every completed body whose condition was true; the body itself must terminate.^[ref]

The prefix maximum correctness example uses $V=n-k$. It counts unread entries and is independent of whether the new entry changes the maximum. Ties therefore cannot stall progress: $k$ increases even when $\mathrm{best}$ stays the same. An integer bounded below cannot strictly decrease indefinitely, which supplies the missing algorithm termination argument.

Strict decrease and a lower bound are insufficient for arbitrary real numbers. The positive sequence $1,1/2,1/4,\dots$ strictly decreases and is bounded below by zero, but never reaches zero. Choosing an integer measure avoids this failure.