← CatZep/Engineering Guides/The Science of Programming
Dijkstra’s weakest-precondition calculus, as Gries teaches it — a single operator that turns a goal into the exact requirement on the starting state, and with it captures total correctness in one line of algebra.
Student edition · understand, apply, verify
Compute entry requirements backward from a desired output while keeping termination and definedness explicit.
What you should be able to do: Derive a weakest precondition for assignments/sequence and distinguish wp from wlp.
Assumes basic programming, not formal-methods notation. This guide defines the needed notation locally. Scalar proofs use mathematical integers unless stated otherwise; finite arrays require integer valid bounds. Guarded-command notation is not Python syntax. Machine overflow, floats, exceptions, aliasing, and concurrency need additional contracts.
Every proof in The Science of Programming rests on one operator: wp, the weakest precondition predicate transformer, borrowed from Dijkstra’s A Discipline of Programming. It is the mathematical engine behind “develop the program and its proof together.” Given what you want to be true when a command finishes, wp tells you the most permissive thing that must be true before it starts — and it does so by working backward from the goal, which is exactly the direction in which you design. This page defines wp, connects it to Hoare triples, states its healthiness laws, and works a small proof by pushing a postcondition backward through a program.
wp(S, R) for the weakest precondition of command S with respect to postcondition R; {P} S {Q} for a Hoare triple; ⇒ for implication; T/F for the universally true/false predicates. See the book for the full, rigorous treatment.Read these definitions first, or use the linked terms as you go. The examples and limitations are local to this guide; companion pages are optional.
wp(S,Q) is the least restrictive entry predicate guaranteeing S terminates normally and establishes Q in this guide's model. Derive it backward from the result.
Example. For x:=x+3 and Q:x>10, wp is x>7. For division, also require the denominator nonzero.
Boundary. Weakest liberal precondition (wlp) omits termination. Undefined expressions need definedness checks, not just textual substitution.
Replace free variable occurrences by an expression without changing quantified/bound-variable meaning. Rename a binder when necessary to keep an inserted free name free.
Example. For x:=y+1 derive Q[x←y+1]. A ∀y inside Q must not accidentally bind a free y from the replacement.
Boundary. This is expression reasoning, not blind string substitution. Simultaneous assignment evaluates right sides in the old state.
{P} S {Q} relates starting states P, program S, and resulting states Q. Partial correctness permits nontermination; total correctness also proves termination.
Example. {x=2} x:=x+1 {x=3} holds. A never-ending loop can satisfy some partial triples but not a total-correctness promise.
Boundary. Exceptions, concurrency, machine arithmetic, and nondeterminism require a stated model. Finite tests do not prove a universal triple.
A predicate is a true/false statement about values; a state assigns values to variables. A state satisfies P when P evaluates true in it.
Example. P:x≥0 holds in state x=3, not x=−1. 'Array sorted' is a predicate about a sequence.
Boundary. Specify integer/real/array domains. Division and indexing must be defined before reasoning about truth.
Guarded selection can choose any enabled branch. Every enabled choice must preserve correctness. No enabled selection guard aborts; an iteration stops when all guards are false.
Example. Choosing max(x,y) with guards x≥y and y≥x permits either branch on equality.
Boundary. This differs from Python's first-matching if/elif. Check coverage under the precondition/invariant; do not assume fairness unless specified.
Fix a command S and a desired postcondition R. The weakest precondition is defined as a set of starting states:
Read it in one breath: “the weakest precondition under which S is guaranteed to establish R.” Two words carry all the weight.
wp a statement of total correctness, not merely partial correctness. A state belongs to wp(S, R) only if starting S there cannot loop forever, cannot abort, and finishes in R. Nontermination disqualifies a state outright — there is no “if it terminates” escape hatch baked into the definition. So wp answers: from which states will S definitely finish and definitely land in R?wp(S, R) is the largest such set: it is the precondition that admits every state from which the guarantee holds, and no state from which it fails. It is exact, not conservative — nothing valid is left out, nothing invalid is let in.If termination and predicate evaluation are known decidable for the modeled command/input, running it can check that input's result. Arbitrary-program wp membership is not generally decidable; symbolic calculi and restricted models do not solve halting.
The older and more familiar notation is the Hoare triple. The triple {P} S {Q} is an assertion about S:
If P holds in the starting state and S is executed, then Q holds in the resulting state.
There is a fork in what that sentence means, and it matters:
S terminates, Q holds afterward. A program that loops forever satisfies every partial-correctness triple vacuously — it never produces a bad final state because it never produces one at all.S does terminate and Q holds afterward. This is the honest guarantee you actually want, and it is the one Gries and Dijkstra work in.The bridge between the triple and the transformer is a single equivalence — for total correctness:
Unpack it. wp(S, Q) is the set of all states from which S is guaranteed to reach Q. The triple {P} S {Q} holds exactly when every state satisfying P is one of those good states — i.e. when P is contained in wp(S, Q), which as predicates is written P ⇒ wp(S, Q).
The immediate consequence: wp(S, Q) is the weakest valid precondition for establishing Q. Any P that makes the triple true must imply it, and wp(S, Q) itself is the largest P that works (it trivially implies itself). Every other correct precondition is a strengthening of it. This is precisely why deriving wp backward from the postcondition is the engine of program construction: it hands you the exact obligation, not an approximation, at every step. The assignment axiom and the loop rules that build on this appear in the commands and their wp and the loop and its invariant.
The name predicate transformer is literal. Each command S is read not as a state-to-state action but as a function on predicates: it maps a postcondition to a precondition.
The direction is the whole point. The machine runs forward — from an input state, through S, to an output state. Reasoning with wp runs backward — from the goal R you want at the end, back to the requirement at the start. You begin with the answer and derive the question. For sequential composition this backward flow is mechanical: wp(S1 ; S2, R) = wp(S1, wp(S2, R)) — you transform R through S2 first, then push the result through S1, right-to-left, opposite to execution order.
There is a dual transformer that runs the other way. The strongest postcondition sp(S, P) is the strongest (smallest, most informative) predicate Q such that {P} S {Q} holds — it takes a precondition and pushes it forward to describe exactly the set of states S can produce from P. The two are linked through the triple: {P} S {Q} holds iff P ⇒ wp(S, Q) and (for partial correctness) iff sp(S, P) ⇒ Q.
Both are valid semantics, but Gries deliberately builds the discipline on wp, not sp. The reason is directional: program development starts from a known goal (the postcondition, the specification) and searches for code and preconditions that reach it. A backward transformer matches that search — you always have the target in hand and ask what must precede it. Forward reasoning with sp is natural for analyzing an existing program (given the input, what comes out?) but awkward for synthesizing one, because you would be computing outputs while still hunting for the code that should produce them. For deriving programs from specifications, wp is the right tool.
Dijkstra observed that anything deserving to be called a command must have a wp obeying a handful of laws — the healthiness properties. They are simultaneously a sanity check on candidate semantics and a working toolkit for proofs.
| Law | Statement | Meaning & why it holds |
|---|---|---|
| Law of the Excluded Miracle | wp(S, F) = F | F is the impossible postcondition — the empty set of states. No command can finish in a state that satisfies F, because there are none. So no starting state can guarantee it, and the precondition is empty too. A command that could establish F would be a “miracle”; the law forbids miracles. |
| Distributivity of conjunction | wp(S, Q) ∧ wp(S, R) = wp(S, Q ∧ R) | Conjunction distributes because every permitted terminating outcome must satisfy both goals. This reasoning also holds for demonic nondeterminism; it does not require a unique outcome. |
| Monotonicity | if Q ⇒ R then wp(S, Q) ⇒ wp(S, R) | A weaker goal has a weaker (or equal) requirement. If reaching Q already implies reaching the laxer R, then any state guaranteeing Q also guarantees R, so wp(S,Q) sits inside wp(S,R). Intuitively: asking for less can never demand more. (This follows from ∧-distributivity, since Q ⇒ R means Q ∧ R = Q.) |
| Distributivity of disjunction | Disjunction equality holds for deterministic commands; it can fail for nondeterministic commands. It is not a characterization of determinism in every observational model. | If a state guarantees Q, or guarantees R, it certainly guarantees Q∨R, so the implication always holds. The converse can fail under nondeterminism: a state might guarantee Q∨R (every run lands in one or the other) yet guarantee neither individually, because different runs choose differently. For a deterministic S there is only one run, so “reaches Q∨R” forces “reaches Q” or “reaches R,” and equality returns. Nondeterminism strictly weakens the left side. |
A useful corollary of the first two: because wp distributes over ∧ and respects implication, computing the wp of a conjunctive postcondition is just conjoining the wp of each part — the everyday move when a specification is a bundle of clauses.
Here is the calculus in action on the classic three-assignment swap. We want to prove the total-correctness triple
where X and Y are fixed logical constants naming the initial values. By the Hoare–wp bridge, proving the triple means proving the precondition implies wp of the whole body with respect to the postcondition. We compute that wp by pushing the postcondition right-to-left through the three assignments, using the assignment rule wp(“v := e”, R) = R[v := e] (substitute e for v in R) at each step.
# Goal R: x = Y and y = X
# Push R backward through t := x ; x := y ; y := t
# Step 1 — through the LAST statement y := t
wp("y := t", x = Y ∧ y = X)
= (x = Y ∧ y = X)[y := t] # replace y by t
= (x = Y ∧ t = X)
# Step 2 — through the MIDDLE statement x := y
wp("x := y", x = Y ∧ t = X)
= (x = Y ∧ t = X)[x := y] # replace x by y
= (y = Y ∧ t = X)
# Step 3 — through the FIRST statement t := x
wp("t := x", y = Y ∧ t = X)
= (y = Y ∧ t = X)[t := x] # replace t by x
= (y = Y ∧ x = X)
# Result: wp(whole body, R) = x = X and y = YThe symbolic argument proves the claim within its stated model; executable boundary/regression tests complement it when translating to a runtime.
A valid triple stays valid if you make its precondition harder to satisfy or its postcondition easier to satisfy. This is the rule of consequence, and it is what lets you connect a computed wp to the specification you were actually handed.
Two independent moves, either or both:
| Move | Rule | Why it is safe |
|---|---|---|
| Strengthen the precondition | replace P by any P' with P' ⇒ P | A stronger precondition describes a smaller set of starting states — a subset of those already known good. If S works from every P-state, it works from every P'-state too. You may always ask for more up front. |
| Weaken the postcondition | replace Q by any Q' with Q ⇒ Q' | A weaker postcondition is a larger, laxer target. If every run lands in Q, it certainly lands in the more permissive Q'. You may always promise less at the end. (This is exactly monotonicity of wp viewed through the triple.) |
The tie-back to wp: since wp(S, Q) is the weakest precondition, any correct P for a given Q is a strengthening of it — the consequence rule’s left half is just the statement P ⇒ wp(S, Q) in disguise. In practice you compute wp(S, Q), then discharge the gap between your given precondition and it with a single implication, exactly as the swap proof did. This same weakening move is what lets a loop invariant plus a false guard imply the postcondition — see the loop and its invariant.
Work through the state changes and the exact claim being checked.
| Step | Evidence, decision, and expected result |
|---|---|
| Set the goal | After x:=x+1; x:=2×x, require x>10. |
| Push through the last assignment | Before doubling, require 2×x>10, or x>5. |
| Push through the first assignment | Before incrementing, require x+1>5, or x>4 over mathematical integers. |
| Check definedness and runtime | The integer model has unbounded arithmetic. A fixed-width implementation needs overflow conditions; a division expression additionally needs a nonzero denominator. |
No. Under demonic nondeterminism, every enabled behavior must terminate and establish the goal.
Download guide_labs.py. Python 3.10+, standard library only. In its directory, run:
python3 guide_labs.py wp
python3 guide_labs.py testThe complete standard-library lab checks the stated finite cases and boundary inputs. Its invariants explain the reasoning; tests alone do not prove all possible inputs.
The program tests its stated finite contracts. It is an educational model, not an implementation of the named production product or a proof of unmodeled distributed faults.
| Idea | The one-line takeaway |
|---|---|
Definition of wp(S, R) | The set of all states from which S is guaranteed to terminate in R — total correctness in one operator. |
| “Weakest” | The most permissive (largest) precondition that still works — exact, not conservative. |
| Hoare triple | {P} S {Q}: if P and S runs, then Q after — partial (if it terminates) vs. total (it does). |
| The bridge | {P} S {Q} ⇔ P ⇒ wp(S, Q); so wp(S,Q) is the weakest valid precondition. |
| Predicate transformer | S is a function from postconditions to preconditions; wp works backward from the goal. |
vs. sp | sp(S,P) pushes forward (strongest post); Gries prefers backward wp for program derivation. |
| Excluded miracle | wp(S, F) = F — nothing can reach the impossible. |
| ∧-distributivity | wp(S,Q) ∧ wp(S,R) = wp(S, Q∧R) — split compound goals freely. |
| Monotonicity | Q ⇒ R gives wp(S,Q) ⇒ wp(S,R) — a weaker goal has a weaker requirement. |
| ∨-distributivity | wp(S,Q)∨wp(S,R) implies wp(S,Q∨R). Equality holds for deterministic commands and can fail under nondeterminism; it is not a universal iff characterization of determinism. |
| Proving a triple | Push the postcondition right-to-left through the statements; check P ⇒ the result. |
| Consequence rule | Strengthen the precondition, weaken the postcondition — validity is preserved. |
wp turns correctness into algebra. Once a command’s weakest precondition is known, every question about it — does this triple hold? what must be true before? — reduces to computing a predicate and checking one implication. Reasoning backward from the goal is not just a proof technique; it is the shape of program design itself.