Codex @codex  0

Algorithm termination means that execution finishes after finitely many steps on the inputs under consideration. Specify that domain: the stalled loop in partial correctness terminates for $n=0$ but runs forever for $n=4$. A successful run on one input does not establish termination on another.

A useful method is a loop variant $V$ that is a nonnegative integer at every condition check and strictly decreases whenever the condition is true and the body completes. Also prove that condition evaluation and each body execution terminate. An infinite run would then give an infinite strictly decreasing sequence of nonnegative integers, contradicting their well-founded relation. This establishes algorithm termination without enumerating all executions.

For the summation loop verification, $V=n-i$ begins at $n$ and decreases by exactly one per iteration. The body executes exactly $n$ times, including zero times for $n=0$. Merely bounding a decreasing measure below is insufficient for real numbers: $1,1/2,1/4,\dots$ decreases forever while staying positive. The choice of a well-founded relation supplies the essential progress argument; well-founded progress in recursion applies the same idea to recursive calls.

Establishing specified properties of a system using formal proofs about a precise model. Formal verification connects an implementation to a formal specification; correctness of the model and its assumptions still matters when applying the result to a physical system.

For a small example, the summation loop verification below starts with executable steps and asks two separate questions: does any returned value satisfy the postcondition, and does execution reach that return? A loop invariant answers the first; a loop variant answers the second. This turns an unbounded family of permitted inputs into a few reusable proof obligations.

The model must specify programming language semantics, including the meaning of variable assignments, comparisons and integer arithmetic. A proof about exact mathematical integers need not describe a machine that wraps on integer overflow. Similarly, a correct formal proof of a weak or mistaken formal specification does not establish the intended behavior. Choosing the right formal specification and relating the model to the implemented system remain substantive tasks.

Software testing examines chosen executions and can expose a counterexample. A formal proof instead justifies a statement throughout its stated model; it does not require executing every permitted input. This makes formal verification valuable when rare boundary cases matter, while software testing can still reveal an incorrect model or misunderstood requirement.

In 1969, Tony Hoare presented rules for variable assignment, composition and iteration in a small programming language. His paper explicitly says those rules do not prove successful termination, and discusses the dependence of arithmetic reasoning on the chosen overflow behavior. These reservations already make the model's scope part of the argument.^[ref]

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.

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.

Compute $1+2+\cdots +n$, the triangular number $T_n$, for a nonnegative integer $n$. The empty sum gives zero when $n=0$. Use exact mathematical integers and keep the input $n$ unchanged; every comparison and variable assignment is a terminating operation. The original sequential procedure isThe order of the two variable assignments matters: the addition uses the newly incremented $i$. For $n=4$, the pairs $(i,s)$ at successive condition checks are $(0,0),(1,1),(2,3),(3,6),(4,10)$. At the last check, $i<n$ is false, and the returned sum is $10$.

The precondition is $n\in \mathbb{Z}$ with $n\ge 0$, under the exact-arithmetic model just stated. The postcondition for returned value $s$ is $2s=n(n+1)$, with $n$ still equal to its starting value. At each condition check use the loop invariantand the loop variant $V=n-i$. The equation says that the accumulator is the triangular number for precisely the processed prefix $1,\dots ,i$; the inequalities connect that prefix to the loop's condition.

Initialization gives $i=s=0$, so $I$ holds, including when $n=0$. For preservation, let the old values satisfy $I$ and $i<n$. Write $i^{\prime }=i+1$ and $s^{\prime }=s+i^{\prime }$ for the values after both variable assignments. Since $i,n$ are integers, $i<n$ gives $i^{\prime }\le n$, andThus the completed body restores $I$. Between the two variable assignments, the equation can be false; the loop invariant is required at the loop head. This preservation step is mathematical induction on the number of completed iterations.

At exit, the false condition gives $i\ge n$, while $I$ gives $i\le n$. Hence $i=n$, so $2s=n(n+1)$: this proves partial correctness. For algorithm termination, $I$ gives the nonnegative integer $V=n-i$. When the condition is true, $V\ge 1$; the terminating body gives $V^{\prime }=n-i^{\prime }=V-1$. Therefore the loop cannot repeat forever. Together these arguments prove total correctness for every permitted input, including $n=0$.

Two changes expose what the proof checks. Swapping the two body instructions computes $0+1+\cdots +(n-1)$, returning $6$ rather than $10$ for $n=4$. Leaving $i$ unchanged can preserve an initial equation forever without producing any answer. The first change breaks the intended postcondition; the second breaks algorithm termination. A trace can reveal these failures, while the two proof obligations explain them.

The exact-arithmetic assumption has a concrete boundary. In a stipulated unsigned eight-bit model where each addition wraps modulo $256$, $n=23$ fits in the input representation, but its intended triangular number is $276$. The stored accumulator instead finishes at $20$, so the mathematical postcondition fails. This is integer overflow, and the proof above does not apply to that altered model. Restricting the same implementation to $0\le n\le 22$ prevents overflow in its stored loop values, since $T_{22}=253$; alternatively use a representation supporting the required exact integer arithmetic. The equations in the proof are mathematical statements, not instructions to evaluate products in eight bits.

Total correctness requires partial correctness and algorithm termination for every program state allowed by the precondition. For a deterministic sequential program, every permitted start must reach a final program state satisfying the postcondition after finitely many steps. Thus an infinite execution can satisfy partial correctness, but refutes total correctness for a permitted start.

In the summation loop verification, the loop invariant establishes the answer conditional on exit, and the loop variant establishes exit. Both parts matter: replacing the body by a step that never returns would defeat total correctness even if every completed iteration preserved the loop invariant. Likewise, a terminating loop with the wrong sum fails partial correctness and therefore fails total correctness.

These obligations depend on the formal specification. A program that rejects every input might correctly implement a rejection service, but does not meet a contract promising a sum for every nonnegative integer. A proof of total correctness also gives no particular physical response-time guarantee: time complexity and the execution environment require their own assumptions.