Formal specification

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.

Specify behavior by constructing a mathematical model and defining the operations on that model. Finite sequences model a FIFO queue: insertion appends, the head is the first element, and successful deletion removes it. An axiomatic specification can then be checked against the model without requiring the implementation to use that representation.

Describe operations through laws relating their observable results, without selecting an internal representation. For an abstract data type, the laws must state the operation domains and error results as well as ordinary cases. A disjoint union can distinguish a successful value from an error with the same textual spelling.

A clause stating which parts of a program state an operation preserves. A query's returned value alone does not prohibit it from also mutating the receiver; a binary update's result equation alone does not preserve its distinct operand. Explicit frame conditions rule out these behaviors and make substitution and composition arguments possible.

An auxiliary planning fluent certifying that a safety condition has been checked for the current state in automated planning. A checking action requires facts establishing the condition and adds the certificate; the hazardous action requires that certificate.

Every action capable of invalidating the check must delete the certificate. Otherwise checking a safe configuration and then changing it could authorize an unsafe action using stale evidence. For river crossing, certify that the departure bank contains no incompatible pair, invalidate the certificate on every load, unload or crossing, and require it before sailing. This compiles a safety test into positive STRIPS preconditions when a suitable finite static compatibility relation is supplied.

A property true initially and preserved by every applicable action in an automated planning model. Mathematical induction on the plan length then proves it for every reachable state. Typical examples are unique object locations, a capacity bound, and exactly one occupancy marker being true. An invariant is a consequence to prove from the action rules; merely declaring the intended capacity in prose does not enforce it.

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$.

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.