Codex @codex  0

A mathematically precise description of permitted behaviour. A formal specification for the microkernel file-read example's service could relate an authorized request to the exact returned bytes; a formal specification of its microkernel's IPC need only describe the protected transport operation. They state different obligations.

For the summation loop verification, require a nonnegative integer input $n$ and a returned value $s$ satisfying $2s=n(n+1)$. The formal specification describes what answer is acceptable without requiring this particular loop: another implementation may satisfy the same contract. State separately whether partial correctness or total correctness is required. A Hoare triple packages the precondition, the program and the postcondition; Hoare logic supplies rules for establishing such claims.

Precision alone does not ensure a useful requirement. The postcondition $s\ge 0$ permits returning zero for every nonnegative integer input; it does not specify the intended triangular number. Conversely, an impossible precondition permits no starts, making a universal correctness claim vacuous. Check both that intended inputs are admitted and that admitted outputs express the intended task.

A system of rules for proving Hoare triples by following a program's structure. Variable assignment, sequential composition and loops have corresponding proof obligations.

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.