← Back to System Internals

The Predicate Transformer wp

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.

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.

Definition

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.

• “Guaranteed to terminate.” This is what makes 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?
• “Weakest.” Recall that a predicate names a set of states, and weaker means a larger set (more permissive). 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.

Because it is a set of states, wp(S, R) is itself a predicate. For a deterministic terminating command S, membership is decidable in principle by running S; the value of the calculus is that you compute the predicate symbolically, without running anything.

Hoare triples and how they relate

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:

• Partial correctness. If 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.
• Total correctness. 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 predicate transformer view

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.

Contrast: the strongest postcondition sp

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.

The healthiness / basic properties

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.

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.

Using wp to prove a triple

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 = Y

The computed weakest precondition is x = X ∧ y = Y — identical to the stated precondition. So the proof obligation P ⇒ wp(S, Q) becomes (x = X ∧ y = Y) ⇒ (x = X ∧ y = Y), which is trivially true. The triple holds, and the swap is proven correct — no test cases, no tracing execution, just substitution. (Assignment’s domain condition and the full command rules are detailed in the commands and their wp.)

Weakening and strengthening

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:

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.

Summary