Codex @codex  0

Partial correctness means that every terminating execution begun in a program state satisfying the precondition $P$ finishes in a program state satisfying the postcondition $Q$. For a sequential program $C$, the usual Hoare triple notation isHere the notation expresses partial correctness; it makes no promise that $C$ finishes. The precondition and postcondition describe permitted starting circumstances and required final circumstances, rather than tests performed automatically by the program.^[ref]

For a sharp example, take the precondition $n=4$ and the following sequential program over mathematical integers:The condition remains true, so execution never reaches the instruction after the loop. Consequently its partial correctness claim holds for the postcondition $2s=n(n+1)$, and even for the impossible postcondition $0=1$: there is no terminating execution with a wrong final result. This is vacuous truth, not evidence that the loop computes a sum. The same program fails total correctness for this permitted input.

The distinction is useful in a proof: first show that an answer, whenever produced, is right; then establish algorithm termination. The summation loop verification supplies both arguments for a loop that actually progresses. Its finite trace illustrates one execution, while its loop invariant covers every permitted input.

The condition required of a final program state when a program finishes under its precondition. The summation loop verification requires returned value $s$ to satisfy $2s=n(n+1)$ and preserves the input $n$. Relating the answer to the original input matters: allowing the program to replace $n$ by zero would change the intended contract.

A postcondition alone gives no promise of algorithm termination. It also need not specify a unique output: $s\ge 0$ allows many answers, while the exact triangular number equation determines one integer answer for each permitted $n$. Stronger postconditions express more obligations; proving only a weaker consequence cannot justify the stronger requirement.

The condition required of a starting program state for a stated correctness guarantee. In the summation loop verification, $n\in \mathbb{Z}$ and $n\ge 0$ admit $n=0$ and $n=4$, but exclude $n=-1$. The accompanying model assumes exact integer arithmetic and terminating elementary operations. The initial values of $i,s$ need no restriction because initialization overwrites them before use.

A precondition is a logical assumption, not automatically an executable check. Writing require in a procedure states its contract; an implementation that checks or rejects invalid inputs needs that behavior specified too. Weakening a precondition admits more starts and therefore demands more proof: dropping $n\ge 0$ here makes $n=-2$ a terminating counterexample to $2s=n(n+1)$, since initialization returns zero while $n(n+1)=2$.

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.