 Prefix maximum correctness example

Given a nonempty finite sequence $a=(a_0,\dots ,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\ge 1$ and exact, terminating integer comparisons and variable assignments. The postcondition for returned value $r$ isThus 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$: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$.

At each condition check, use the loop invarianttogether 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 isThe variable assignment $k\leftarrow 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\ge n$, while $I$ gives $k\le 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\ge 1$. 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.