= Prefix maximum correctness example
Given a nonempty finite <sequence> $a=(a_0,\ldots,a_{n-1})$ of <integers>, return its <maximum> value. Represent the <sequence> by an <array> whose contents remain unchanged during execution. The <precondition> requires an <integer> length $n\geq1$ and exact, terminating <integer> comparisons and <variable assignments>. The <postcondition> for returned value $r$ is
$$
r\in\{a_i:0\leq i<n\}\quad\text{and}\quad a_i\leq r\ \text{for every }0\leq i<n.
$$
Thus the <output> belongs to the <finite set> of entries and is at least every entry. The contract permits ties and negative <integers>; it asks for a value, not the position of a particular occurrence. There is no <maximum> of an empty <set> of <integers>, so empty <input> is deliberately outside this <precondition>. A service accepting empty <inputs> needs a different <formal specification>, such as a separate absent result.
This <Python> implementation makes the <variable assignments> explicit. Its index arithmetic models exact <integer> arithmetic; fixed-width implementations additionally need enough index range for $n$:
``
def find_max(a):
n = len(a)
best = a[0]
k = 1
while k < n:
if a[k] > best:
best = a[k]
k = k + 1
return best
``
For the original <input> $[3,1,4,4,2]$, initialization gives $k=1$ and $\mathrm{best}=3$. Reading $a_1=1$ keeps $3$; reading $a_2=4$ changes it to $4$; reading $a_3=4$ and $a_4=2$ keeps $4$. At successive condition checks, the pairs $(k,\mathrm{best})$ are $(1,3),(2,3),(3,4),(4,4),(5,4)$. The returned <maximum> is $4$.
\Image[/prefix-maximum-invariant-trace.png]
{title=<Maximum> values of successive prefixes in the original <integer> <array>}
{description=Each row shows the processed prefix of $[3,1,4,4,2]$ immediately before checking $k<n$. Blue cells have been processed; grey cells have not. The <loop invariant> records the <maximum> of the blue entries, while the <loop variant> $n-k$ counts remaining entries. These are exact constructed execution states.}
At each condition check, use the <loop invariant>
$$
I:\qquad 1\leq k\leq n,\qquad \mathrm{best}=\max\{a_i:0\leq i<k\},
$$
together with the fact that the <input> <array> is unchanged. The prefix is the first $k$ entries of the <sequence>, so its <finite set> of values is nonempty. The <maximum> need not be unique as an occurrence: the invariant concerns its value.
Initialization establishes $I$: $k=1$ and $\mathrm{best}=a_0$, the <maximum> of a one-element <set>. For preservation, suppose $I$ and $k<n$ hold. Then $a_k$ is a valid <array> entry. Either the comparison replaces $\mathrm{best}$ with the larger value $a_k$, or it keeps a value at least $a_k$. Before increasing $k$, the resulting value is
$$
\max\bigl(\max\{a_i:0\leq i<k\},a_k\bigr)=\max\{a_i:0\leq i<k+1\}.
$$
The <variable assignment> $k\gets k+1$ restores the complete <loop invariant>. Between the two <variable assignments>, the old prefix formula may temporarily be false; the <loop invariant> is required at condition checks, not at every instruction.
At exit, $k\geq n$, while $I$ gives $k\leq n$. Hence $k=n$, and $I$ gives exactly the required <postcondition>. This establishes <partial correctness>. The preservation argument is <mathematical induction> on the number of completed iterations, covering every permitted <integer> <sequence>, rather than just the pictured <input>.
For <algorithm termination>, the <loop variant> $V=n-k$ is a nonnegative <integer> whenever $I$ holds. If $k<n$, then $V\geq1$. Every body terminates under the <precondition> and changes $V$ to $V-1$. Starting at $n-1$, it reaches zero after exactly $n-1$ iterations. For $n=1$, the initial value is already zero and the body is never entered. Together with <partial correctness>, this proves <total correctness>.
Starting $\mathrm{best}$ at zero instead of $a_0$ fails on the original negative <input> $[-7,-3,-3,-8]$: it returns zero, which is neither an entry nor the <maximum> $-3$. Keeping $k=1$ forever preserves the correct initial prefix claim but loops forever when $n>1$; a <loop invariant> alone does not ensure <algorithm termination>. Using `>=` instead of `>` still returns the same <maximum> value when entries tie, although a version returning a position would need an explicit tie rule.
Back to article page
