Verification, run backward, as a calculation. Given a program C and a goal Q, the predicate transformer wp(C, Q) returns the weakest assertion P for which {P} C {Q} holds — the exact set of start states from which C is guaranteed to land in Q. No search, no guessing: you push Q back through the program, one construct at a time. Down the center, data flows: the goal goes in, wp calculates backward, the precondition comes out. The blue team builds and defends; the red team attacks.
source E. W. Dijkstra, Guarded Commands, Nondeterminacy and Formal Derivation of Programs, CACM 18(8):453–457 (1975) — doi:10.1145/360933.360975. Rendered, not quoted.
wp is defined by one rule per construct. Each is a mechanical rewrite on predicates — no state is ever run forward:
| construct | wp(C, Q) |
|---|---|
| skip | Q |
| x := e | Q[x := e] |
| C₁ ; C₂ | wp(C₁, wp(C₂, Q)) |
| if b then C₁ else C₂ | (b ∧ wp(C₁,Q)) ∨ (¬b ∧ wp(C₂,Q)) |
Assignment is a substitution. Sequence is composition, right first. The conditional splits on the guard. Read bottom-up, these are the whole engine — verified exhaustively over a 9-state space, never looked up.
A triple {P} C {Q} (the-hoare-logic) says nothing about how weak P can be. Dijkstra makes the answer canonical:
{P} C {Q} is valid if and only if P ⇒ wp(C, Q). So wp(C,Q) is the single weakest — largest — precondition, and every valid P is one of its subsets. Hoare's proof rules become a backward calculation: the weakest assumption that still guarantees the goal.
The blue team's live check: over all 4 programs × 4 goals, confirm the syntactic wp equals the true semantic preimage (states that actually reach Q). If red tampers with the sequence rule, this badge is where it shows.
The state space is finite and total: two variables x, y ∈ {0,1,2}, arithmetic mod 3 — exactly 9 states. A predicate is just the set of states that satisfy it. A program is one of:
| C | means |
|---|---|
| x := e | set x to e (mod 3) |
| C₁ ; C₂ | do C₁, then C₂ |
| if b … | branch on guard b |
Pick a goal Q and a program C below; the panel pushes Q backward and hands you the precondition. Loop-free by construction, so every claim is exhaustively decidable.
Change program or goal — wp is computed from the four rules on the spot. The backward calculation is shown; nothing is table-lookup.
| x\y | 0 | 1 | 2 |
|---|
What the machine proves: for every program/goal here, the syntactic wp(C,Q) equals the exact set of start states from which C reaches Q — and it is the largest such set, so it is genuinely weakest. The current wp is above; the fact that it is sound and weakest is the output.
The blue team's witness (left) confirms this live over all cases; the red team (right) tries to make wp lie.
Two more honest edges: this is total-correctness wp (it demands termination — the weaker wlp does not); and for demonic nondeterminism, wp takes the conjunction over all outcomes, not a lucky one. Over an infinite state space none of these sets can be verified by enumeration — the exhaustive checks here are a courtesy of the finite domain, not a general proof.
"wp is just running the program backward." Cut. It transforms predicates (sets of states), not single states; a program need not be invertible. wp(x:=0, x=0) is true — every state qualifies — though x:=0 is not a bijection.
"For a sequence, take the union of the two preconditions." Cut. It is functional composition, right operand first: wp(C₁, wp(C₂, Q)). Reversing the order (window 6) yields a different, wrong set.
"wp and Hoare logic are rival methods." Kept, corrected. {P}C{Q} is valid iff P ⇒ wp(C,Q); wp is Hoare's calculus turned mechanical, the weakest P its canonical witness.
The red team's move: compute the sequence rule in the wrong order — wp(C₂, wp(C₁, Q)) instead of wp(C₁, wp(C₂, Q)). For an order-sensitive program the result is no longer the weakest precondition. The blue team's witness (window 7) is watching.
Swap the order and wp(x:=x+1 ; x:=x·2, x=0) reports the wrong set — x=1 instead of the true x=2. The witness recomputes, disagrees with the semantic preimage, and turns red. Nothing is faked; the attack is real and it is caught.