= Partial correctness
<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 is
$$
\{P\}\ C\ \{Q\}.
$$
Here 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.<An Axiomatic Basis for Computer Programming by Tony Hoare>[Hoare, 1969, §3 Program Execution, p. 577, and §4 General Reservations, pp. 578–579; the paper instead labels the precondition P, program Q and result R]{ref}
For a sharp example, take the <precondition> $n=4$ and the following sequential program over mathematical <integers>:
``
i = 0
s = 0
while i < n:
i = i
``
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>.
Back to article page
