= Loop variant
{title2=$V$}
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.<CS 2112 Fall 2019/Loop invariants>[CS 2112 Fall 2019; Loop invariants, Using loop invariants to show code is correct: Termination and the decrementing function]{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.
\Image[/prefix-maximum-proof-obligations.png]
{title=Control flow and four proof obligations for the <prefix maximum correctness example>}
{description=Initialization, preservation, and exit establish <partial correctness>; the <loop variant> establishes <algorithm termination> and hence <total correctness>. The <loop invariant> is restored after both <variable assignments>. The <input> <array> stays unchanged throughout.}
Strict decrease and a lower bound are insufficient for arbitrary <real numbers>. The positive <sequence> $1,1/2,1/4,\ldots$ strictly decreases and is bounded below by zero, but never reaches zero. Choosing an <integer> measure avoids this failure.
Back to article page
