Weakest Preconditions
Hoare logic
gives us a proof system, but it leaves a nagging freedom: at every step we must guess the
intermediate assertions and then check them. Edsgar Dijkstra's insight, in his 1975 predicate
transformer calculus, was to remove the guessing for straight-line code entirely. Instead of
proposing a precondition and verifying it, compute the best one directly, working
backwards from the goal.
For a command c and a desired postcondition Q,
the weakest precondition
\mathrm{wp}(c, Q)
is the most permissive assertion on the initial state that guarantees: running
c terminates and ends in a state satisfying Q.
"Weakest" is the key word — it captures every starting state from which
c is bound to achieve Q, and no state from which
it might fail. It is the exact boundary of success.
Weakest of what, exactly?
Recall from the previous page that assertions are ordered by implication:
P_1 \Rightarrow P_2 means P_1 is
stronger (rules out more states, sits lower in the lattice), P_2
weaker (higher). Among all preconditions that make the Hoare triple valid, wp is the
weakest — the greatest in the implication order.
\mathrm{wp}(c, Q) is characterised by two facts:
-
It works: the total-correctness triple
[\,\mathrm{wp}(c,Q)\,]\; c\; [\,Q\,] holds.
-
It is weakest: for any assertion P, the triple
[\,P\,]\; c\; [\,Q\,] holds if and only if
P \Rightarrow \mathrm{wp}(c, Q).
That "if and only if" turns verification into a single implication check. To prove
[P]\, c\, [Q], compute \mathrm{wp}(c, Q) by the
rules below, then discharge one logical obligation
P \Rightarrow \mathrm{wp}(c, Q) — the verification condition.
No cleverness required for the program part; all the difficulty is concentrated into a formula a theorem
prover can attack.
In the lattice above, every valid precondition for Q lies below
\mathrm{wp}(c,Q); wp is the ceiling of that region — the single highest point
from which c still guarantees Q.
The predicate-transformer rules
\mathrm{wp}(c, \cdot) is a predicate transformer: it maps a
postcondition to a precondition, i.e. a function from assertions to assertions. Dijkstra gave it by
recursion on the command, and the rules read straight off the Hoare rules run backwards.
\mathrm{wp}(\mathtt{skip}, Q) \;=\; Q
\mathrm{wp}(x := a, Q) \;=\; Q[a/x]
\mathrm{wp}(c_1 ; c_2, Q) \;=\; \mathrm{wp}\big(c_1,\ \mathrm{wp}(c_2, Q)\big)
\mathrm{wp}(\mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2,\ Q) \;=\; \big(b \Rightarrow \mathrm{wp}(c_1, Q)\big) \wedge \big(\neg b \Rightarrow \mathrm{wp}(c_2, Q)\big)
Three of these are pure mechanism. The assignment rule is the Hoare assignment axiom, now read as a
computation: to guarantee Q after x := a,
substitute a for x in
Q. The sequencing rule is the jewel: push
Q back through c_2 first, then through
c_1 — backwards, right to left, exactly the reverse of execution
order. And the conditional splits into "whichever branch runs must establish
Q".
Backward substitution in action
Watch wp flow through a two-assignment block. We want the postcondition
Q \equiv (x > y) after x := x + 1;\ y := 0.
Compute right-to-left.
-
Innermost first (y := 0):
\mathrm{wp}(y := 0,\ x > y) = (x > y)[0/y] = (x > 0).
-
Then (x := x+1):
\mathrm{wp}(x := x+1,\ x > 0) = (x > 0)[x{+}1/x] = (x + 1 > 0) = (x \ge 0).
So \mathrm{wp}(x := x+1;\ y := 0,\ x > y) = (x \ge 0).
Read the result: the block ends with x > y exactly when it started with
x \ge 0 — nothing weaker will do (start at
x = -1 and you finish with x = 0, y = 0,
violating x > y), and nothing stronger is necessary. wp found the exact
boundary with pure substitution.
Loops: an invariant and a variant
A loop has no finite backward expansion — you cannot push Q through
infinitely many unfoldings. So, exactly as in Hoare logic, wp for a loop requires human input: an
invariant I for correctness and a
variant (a well-founded ranking function) for termination. Verification-condition
generation then reduces the annotated loop to a fixed set of implications to prove.
To establish the total-correctness triple
[\,P\,]\; \mathtt{while}\ b\ \mathtt{do}\ c\; [\,Q\,] with invariant
I and integer variant V, discharge:
- Initiation: P \Rightarrow I.
- Consecution: (I \wedge b) \Rightarrow \mathrm{wp}(c, I)
— the body preserves I.
- Exit: (I \wedge \neg b) \Rightarrow Q.
- Progress: (I \wedge b) \Rightarrow V > 0 and
(I \wedge b) \Rightarrow \mathrm{wp}\big(c,\ V < V_0\big) where
V_0 is V's value before the body — the variant
strictly decreases yet stays bounded below, so the loop cannot run forever.
This is precisely how tools like Dafny, ESC/Java and Why3 work: the programmer writes the invariant and
variant as annotations, a verification-condition generator mechanically produces these
implications by pushing wp through the loop-free fragments, and an SMT solver discharges them. Human
insight for the loop; automation for everything else.
A weakest-precondition calculator
Because wp for loop-free code is mechanical, we can implement it. We represent assertions and
expressions as strings and implement the transformer for skip, assignment, sequencing, and
conditionals — performing the substitution Q[a/x] textually. Then we compute
the weakest precondition of a small program, backwards.
// A tiny command language (loop-free), enough to compute wp mechanically.
type Cmd =
| { kind: "skip" }
| { kind: "assign"; x: string; a: string }
| { kind: "seq"; c1: Cmd; c2: Cmd }
| { kind: "if"; b: string; c1: Cmd; c2: Cmd };
// Substitute expression `a` for every whole-word occurrence of variable `x` in assertion Q.
function subst(Q: string, x: string, a: string): string {
const re = new RegExp("\\b" + x + "\\b", "g");
return Q.replace(re, "(" + a + ")");
}
// wp(c, Q) — the weakest precondition, computed by recursion on the command.
function wp(c: Cmd, Q: string): string {
switch (c.kind) {
case "skip":
return Q; // wp(skip, Q) = Q
case "assign":
return subst(Q, c.x, c.a); // wp(x:=a, Q) = Q[a/x]
case "seq":
return wp(c.c1, wp(c.c2, Q)); // push Q back through c2, then c1
case "if":
return `((${c.b}) => ${wp(c.c1, Q)}) && (!(${c.b}) => ${wp(c.c2, Q)})`;
}
}
// Program: x := x + 1 ; y := 0 with postcondition x > y
const prog: Cmd = {
kind: "seq",
c1: { kind: "assign", x: "x", a: "x + 1" },
c2: { kind: "assign", x: "y", a: "0" },
};
console.log("wp(x:=x+1 ; y:=0 , x > y) = " + wp(prog, "x > y"));
// Program: if (x >= 0) then m := x else m := -x with postcondition m >= 0
const absProg: Cmd = {
kind: "if", b: "x >= 0",
c1: { kind: "assign", x: "m", a: "x" },
c2: { kind: "assign", x: "m", a: "-x" },
};
console.log("wp(if x>=0 then m:=x else m:=-x , m >= 0) = " + wp(absProg, "m >= 0"));
The first result simplifies to x + 1 > 0, i.e.
x \ge 0 — matching our hand calculation. The second is
(x \ge 0 \Rightarrow x \ge 0) \wedge (x < 0 \Rightarrow -x \ge 0), which is
\mathsf{true}: the absolute-value program establishes
m \ge 0 from any starting state, so its weakest precondition is
trivially satisfiable. The calculator is doing verification-condition generation in miniature.
wp as a predicate transformer: the algebra
Dijkstra's calculus is beautiful partly because \mathrm{wp}(c, \cdot) obeys
crisp algebraic laws, independent of the specific command. These are the "healthiness conditions" a
sensible transformer must respect.
- Monotone: if Q_1 \Rightarrow Q_2 then
\mathrm{wp}(c, Q_1) \Rightarrow \mathrm{wp}(c, Q_2) — asking for less
demands no more.
- Conjunctive:
\mathrm{wp}(c, Q_1 \wedge Q_2) = \mathrm{wp}(c, Q_1) \wedge \mathrm{wp}(c, Q_2).
- Excluded miracle:
\mathrm{wp}(c, \mathsf{false}) = \mathsf{false} — no command can
establish the impossible, so nothing guarantees \mathsf{false} (a total,
deterministic command cannot work "miracles").
The excluded-miracle law is a lovely sanity check: if your wp calculation ever yields a
satisfiable precondition for the postcondition \mathsf{false}, you
have a bug in your rules. Monotonicity ties wp back to the domain-theoretic
picture: wp is a monotone map on the lattice of predicates, and — for loops — the loop's wp is itself a
fixed point of an unfolding transformer, closing the circle back to where this module began.
Dijkstra's conviction, delivered with characteristic sharpness, was that "program testing can be
used to show the presence of bugs, but never to show their absence." A test exercises one path
through one state; a program has astronomically many. His predicate-transformer calculus was an attempt
to replace the hopeless task of testing every case with a finite calculation: derive the
weakest precondition, prove one implication, and you have reasoned about all executions at once.
The very phrase "weakest precondition" encodes the ambition — not a precondition that happens
to work, but the exact characterisation of every state from which the program is guaranteed to
succeed. It reframed programming as a goal-directed, backward-from-the-specification activity, a stance
that runs through everything from Hoare logic to modern SMT-backed verifiers like Dafny.
A subtle but crucial distinction. \mathrm{wp}(c, Q) is a
total-correctness transformer: it demands that c
terminates and lands in Q. Its partial-correctness cousin, the
weakest liberal precondition \mathrm{wlp}(c, Q), drops the
termination demand — it holds of any state from which c either diverges or
ends in Q. They agree on loop-free code but part ways on loops:
\mathrm{wlp}(\mathtt{while}\ \mathtt{true}\ \mathtt{do}\ \mathtt{skip},\ Q) = \mathsf{true}
(the loop never breaks Q because it never finishes), whereas
\mathrm{wp}(\mathtt{while}\ \mathtt{true}\ \mathtt{do}\ \mathtt{skip},\ Q) = \mathsf{false}
(it never terminates, so it cannot guarantee anything). Reach for wp when you need the program
to actually finish; reach for wlp when you are only proving "no wrong answers". Mixing them up is how a
"verified" program can still hang forever.