Specifications: Pre- and Postconditions

A specification is a contract, and every contract has two parties. When you call a routine, you promise to hand it inputs it is entitled to expect; in return the routine promises to hand you back a result it guarantees. Name those two promises and you have the whole grammar of formal specification: the caller's obligation is the precondition, the routine's guarantee is the postcondition. Everything else in program correctness is built on this handshake.

On the previous page we said a program is correct when it meets its specification. Here we write the specification down precisely — in predicate logic over the program's variables — and meet the notation that lets us reason about it: the Hoare triple.

The contract: who owes what

The asymmetry is the whole point. A weaker precondition is a better routine — it demands less of callers, so it is usable in more places. A stronger postcondition is a better routine — it guarantees more, so callers can rely on more. And the deal is one-directional: if the caller breaks the precondition, the routine owes nothing — any behaviour whatsoever is "correct," including garbage or a crash. This is why P is a gift to the implementer: it carves off exactly the inputs they are not responsible for.

The Hoare triple

The contract has a two-hundred-character-wide notation, due to Tony Hoare (1969): the Hoare triple

\{P\}\; C \;\{Q\}

read "if P holds before command C runs, and C terminates, then Q holds afterwards." The braces are the specification; C in the middle is the implementation. A triple with the termination proviso is partial correctness; strengthen it to demand that C actually halts and you have total correctness, often written with square brackets [P]\,C\,[Q]. This little object is the sentence of the whole logic — a full calculus of rules for deriving triples is the subject of Hoare logic, which this page is the doorway to.

Two triples that sharpen intuition. The strongest-imaginable spec of the identity is \{x = 5\}\; \texttt{skip} \;\{x = 5\}. And the emptiest promise is \{\texttt{true}\}\; C \;\{\texttt{true}\} — precondition assumes nothing, postcondition guarantees nothing, satisfied by any C at all.

Writing specs in predicate logic

Real postconditions quantify over data. To specify "the routine returns the maximum of a nonempty array a[0..n)", the guarantee has two clauses — the result is an upper bound, and it is actually attained:

P:\; n > 0 \qquad Q:\; \bigl(\forall i.\; 0 \le i < n \Rightarrow r \ge a[i]\bigr) \;\wedge\; \bigl(\exists j.\; 0 \le j < n \wedge r = a[j]\bigr)

Miss the second clause and the constant function r = +\infty satisfies your "maximum" — an upper bound that is never attained is not a maximum. This is the recurring craft of specification: pin the answer down from both sides. A common professional habit is to also mention what must not change — a frame condition such as "the array a is a permutation of its old contents" — because a postcondition that only constrains the return value silently permits the routine to scribble over everything else.

A subtlety of postconditions is referring to old values. "Increment" is not x > 0; it is x = x_{\text{old}} + 1, where x_{\text{old}} names the value on entry. Specification languages give this a keyword — Eiffel's old, JML's \old, Dafny's old(...) — precisely because a guarantee about change must be able to talk about the "before" from within the "after."

Worked spec 1: integer square root

We want \mathrm{isqrt}(n) to return the floor of \sqrt{n} — the largest r with r^2 \le n — using only integer arithmetic. The contract, written as comments right where a reviewer will read them:

// precondition: n >= 0 // postcondition: r*r <= n AND (r+1)*(r+1) > n (r = floor(sqrt n), r >= 0) function isqrt(n: number): number { let r = 0; while ((r + 1) * (r + 1) <= n) { r = r + 1; } return r; // spec pins r between two consecutive squares }

The two-sided postcondition r^2 \le n \wedge (r+1)^2 > n is a textbook pin-from-both-sides: the left clause says r is not too big, the right says it is not too small, and together they determine r uniquely. Note the spec never mentions the while loop — an implementation by Newton's method or binary search would satisfy exactly the same contract, which is the whole reason we specify the relation and not the recipe.

Worked spec 2: array maximum, and the frame

// precondition: a.length > 0 // postcondition: (for all i in [0, a.length): r >= a[i]) -- upper bound // AND (exists j in [0, a.length): r === a[j]) -- attained // AND a is unchanged -- frame condition function maximum(a: readonly number[]): number { let r = a[0]; for (let i = 1; i < a.length; i = i + 1) { if (a[i] > r) r = a[i]; } return r; }

The readonly on the parameter is the type system helping enforce the frame condition: the compiler now refuses any statement that would mutate a, so "a is unchanged" moves from a comment you hope holds to an invariant the language checks. Where a specification can be pushed into the type, it should be — a proof obligation the compiler discharges for free is the cheapest correctness you will ever get.

A teaser: strongest post, weakest pre

For a fixed command C, precondition and postcondition are not independent — one can be computed from the other, in two dual ways.

The triple \{P\}\,C\,\{Q\} is valid exactly when P \Rightarrow \mathrm{wp}(C, Q), equivalently when \mathrm{sp}(P, C) \Rightarrow Q. Dijkstra's insight was that \mathrm{wp} is computable by walking the program backwards, one construct at a time — turning "is this triple valid?" into a mechanical calculation. We develop the weakest-precondition calculus in full later in the course; for now, just hold the picture: sp goes forwards, wp goes backwards, and the spec is valid when they meet in the middle.

Because a precondition of \texttt{true} obliges the routine to work on every input, including the ones it genuinely cannot handle. isqrt with precondition \texttt{true} would have to return a sensible floor-of-a-square-root for n = -7 — but there is no such integer, so either the postcondition becomes a tangle of special cases or the routine is simply unimplementable. The art is to make the precondition as weak as you can while keeping the postcondition achievable and simple. "Weaker is better" is a pull, not an absolute; it is balanced by "the guarantee still has to be deliverable." Push the precondition to \texttt{true} only when the routine really is total — and then celebrate, because a total routine with a strong postcondition is the gold standard.

The single most common misreading of a contract is to think a routine is "buggy" because it misbehaves on input outside its precondition. It is not. If isqrt's precondition is n \ge 0 and you pass -1, then whatever isqrt does — returns nonsense, throws, loops forever — it is still correct with respect to its specification, because the specification made no promise there. The triple \{n \ge 0\}\,\texttt{isqrt}\,\{r^2 \le n < (r+1)^2\} is completely silent about n < 0. If you want a defined behaviour for negatives (say, throw a specific error), that is a different, weaker precondition with an enlarged postcondition — write it into the contract. Do not blame the routine for a promise you never asked it to make. The flip side: a routine that silently returns garbage on a precondition violation is a debugging nightmare, which is exactly why the next page turns preconditions into runtime asserts that fail loudly.