Weakest Precondition Calculus

Origin. Edsger Dijkstra (1975, "Guarded Commands, Nondeterminacy and Formal Derivation of Programs"; 1976 monograph). A predicate-transformer semantics giving each program a function on postconditions, turning correctness reasoning into predicate calculus and supporting the systematic derivation of programs from specifications.

Models. Programs as predicate transformers. Rather than assert Hoare triples directly, each command S is interpreted as a function wp(S, ·) mapping a postcondition R to the weakest predicate on the initial state guaranteeing that S terminates in a state satisfying R. Correctness becomes an implication between predicates; program construction becomes calculation.

Formalism.

Weakest precondition: wp(S, R) = the weakest P such that {P} S {R} holds in the total-correctness sense (S terminates and establishes R). Hoare triple recovered: {P} S {R} iff P ⇒ wp(S, R).

Healthiness conditions (Dijkstra): Law of the excluded miracle: wp(S, false) = false. Monotonicity: R ⇒ Q implies wp(S,R) ⇒ wp(S,Q). Conjunctivity: wp(S, R ∧ Q) = wp(S,R) ∧ wp(S,Q). Disjunctivity (for deterministic S): wp(S, R ∨ Q) = wp(S,R) ∨ wp(S,Q).

Rules for the guarded-command language: skip: wp(skip, R) = R assignment: wp(x := e, R) = R[x ↦ e] sequence: wp(S₁; S₂, R) = wp(S₁, wp(S₂, R)) conditional: wp(if □ᵢ Bᵢ → Sᵢ fi, R) = (∃i. Bᵢ) ∧ ∀i. (Bᵢ ⇒ wp(Sᵢ, R)) loop: wp(do B → S od, R) via an invariant I and a variant (bound function) t decreasing on each iteration and bounded below.

Variants: wp = total correctness (demands termination); wlp (weakest liberal precondition) = partial correctness, dropping the termination requirement (wlp(S,false) may be true). Angelic vs demonic nondeterminism give dual transformers (weakest precondition vs strongest postcondition).

Symbols.

Symbol	Unicode	Meaning
wp(S, R)	—	weakest precondition of S for postcondition R
wlp(S, R)	—	weakest liberal precondition (partial correctness)
R[x ↦ e]	—	substitution of e for x in R
□	U+25A1	guarded-command alternative separator
⇒	U+21D2	predicate implication
I, t	—	loop invariant, variant/bound function

Metatheory. The predicate-transformer semantics is equivalent to Hoare logic but algebraic and compositional: sequencing is function composition, and the healthiness conditions characterize exactly the transformers arising from programs. wp captures total correctness (via the loop bound function), wlp captures partial correctness; strongest-postcondition is the dual transformer. The calculus is the semantic basis for refinement (a specification is refined by any program whose wp is stronger) and for verification-condition generation in automated tools.

Applies to. Formal program derivation and correctness-by-construction. Verification-condition generation (Dafny, Boogie, ESC/Java, Why3). Refinement calculus and specification languages. Teaching rigorous imperative reasoning.

Limitations. Loops still require a manually supplied invariant and variant — the calculus mechanizes bookkeeping, not the creative step. Scales awkwardly to pointers/heap and concurrency without extensions (separation logic, rely-guarantee). Full predicate reasoning is undecidable, so discharging verification conditions needs theorem proving. Nondeterminism semantics (angelic vs demonic) must be fixed carefully.