Hoare logic gives you the rules to verify a program, but it leaves you doing the creative work: at every step you have to guess the assertion in the middle and then check it fits. For a machine that is hopeless — you cannot ask a computer to "have an insight." In the mid-1970s Edsger Dijkstra reorganised the whole logic around a single function that removes the guessing entirely. Give it a command and a goal, and it computes the precondition you need. No search, no cleverness — just substitution, run backwards through the code.

That function is the weakest precondition, written \operatorname{wp}(C, Q). It turns Hoare logic from an art you practise into a calculation you can automate — the foundation of every modern program verifier.

What "weakest" means

Fix a command C and a desired postcondition Q. Many preconditions P might make the triple \{P\}\,C\,\{Q\} valid — but they are not equally good. A precondition that is too strong (demands too much) rules out starting states that would actually have worked. The weakest precondition is the most permissive one: it accepts every starting state from which running C is guaranteed to terminate in a state satisfying Q, and no others.

Think of \operatorname{wp}(C, Q) as describing the largest possible set of safe launch pads. Strengthen it and you throw away good launch pads for no reason; weaken it and you include pads from which the flight might crash or never land.

The equivalence that ties it to Hoare logic

Because \operatorname{wp} captures exactly the safe starting states, checking any Hoare triple collapses into a single implication:

This is the whole trick of automated verification: reduce "does this code satisfy this contract?" to "is this one formula valid?", and hand the formula to a solver.

The rules — one per construct

Each rule tells you how to push a postcondition backwards across one language construct. Applied repeatedly, they walk from the end of the program to the start.

Notice there is no case analysis to invent and no middle assertion to guess. The rules are purely syntactic: they manipulate the text of Q. A program built from these four constructs has its weakest precondition computed, not discovered.

A backward calculation, line by line

Let us verify that a three-line block leaves y holding twice the larger of two inputs — postcondition Q \equiv y = 2\max(a,b). We start at the bottom with Q and drag it upward, applying one rule per line.

Step 2 — assignment y := 2m. Substitute 2m for y in Q:

Step 1 — the conditional with this new goal R \equiv m = \max(a,b). The then branch is m := a, giving \operatorname{wp} = (a = \max(a,b)); the else branch m := b gives (b = \max(a,b)). Assemble:

Both implications are logically true (if a \ge b then indeed a = \max(a,b), and likewise for the other), so the weakest precondition of the whole block reduces to \texttt{true}. The program works for every input — proved, without ever guessing an intermediate assertion. We simply computed.

Liberal preconditions: dropping termination

Sometimes you only care about partial correctness — "if it halts, the answer is right" — and are content to argue termination separately. For that there is the twin transformer, the weakest liberal precondition \operatorname{wlp}(C, Q).

For the loop-free constructs above, \operatorname{wp} and \operatorname{wlp} coincide — no loops, so nothing can diverge. The difference only appears once loops (and their variants) enter the story.