Weakest Preconditions

Every programmer has wondered: what inputs will make this code do the right thing? Answering that question by testing is slow and incomplete. There is a better way.

In 1975, Edsger W. Dijkstra introduced the predicate transformer — a mechanical rule that works backward through a program. You start with the result you want (the postcondition), feed it through the program in reverse, and out comes the weakest precondition: the most permissive description of all inputs for which the program is guaranteed to deliver that result.

"Weakest" here means least restrictive — any stronger condition would unnecessarily exclude valid inputs. The predicate transformer computes exactly the right one, neither too tight nor too loose, by a small set of rules applied to each statement one at a time.

This is not just theory. The same idea powers every modern program verification tool, automated test generators, and the proofs that keep critical software safe.

Choose a simple program and a postcondition. The demo propagates the condition backward through each statement using Dijkstra's rules, revealing the weakest precondition at every step.

<!-- {{c_intro}} -->
<p class="hint">{{hint_para}}</p>
<div class="controls">
  <label>{{label_program}}</label>
  <select id="prog-select">
    <option value="assign1">{{opt_assign1}}</option>
    <option value="assign2">{{opt_assign2}}</option>
    <option value="seq">{{opt_seq}}</option>
    <option value="cond">{{opt_cond}}</option>
  </select>
</div>
<div class="controls">
  <label>{{label_post}}</label>
  <select id="post-select">
    <option value="pos">{{opt_post_pos}}</option>
    <option value="even">{{opt_post_even}}</option>
    <option value="gt10">{{opt_post_gt10}}</option>
  </select>
</div>
<div id="steps-area"></div>
<div class="btns">
  <button id="compute-btn" type="button">{{btn_compute}}</button>
  <button id="reset-btn" type="button" class="ghost">{{btn_reset}}</button>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; padding: 4px; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .7rem; line-height: 1.5; }
.controls { display: flex; align-items: center; gap: .5rem; margin-bottom: .5rem; flex-wrap: wrap; }
label { font-size: .85rem; font-weight: 600; color: #1d3557; white-space: nowrap; }
select { font: 14px system-ui; padding: .3rem .5rem; border: 1px solid #adb1b8; border-radius: 6px;
         background: #fff; color: #222; cursor: pointer; flex: 1; min-width: 0; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-top: .6rem; }
button { font: 600 14px system-ui; padding: .4rem .9rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
#steps-area { margin: .7rem 0; }
.step { background: #f0f4f8; border-left: 3px solid #1d3557; border-radius: 0 6px 6px 0;
        padding: .45rem .7rem; margin-bottom: .4rem; font-size: .88rem; line-height: 1.55; }
.step .stmt { font-family: ui-monospace, monospace; font-weight: 700; color: #1d3557; }
.step .rule { font-size: .8rem; color: #555; font-style: italic; }
.step .pred { font-family: ui-monospace, monospace; color: #0a7d33; font-weight: 600; }
.step-final { background: #e6f4ea; border-color: #0a7d33; }
.step-final .pred { font-size: 1rem; }
.empty-hint { font-size: .9rem; color: #777; margin: .4rem 0; }

// Code not found

Notice how assignment simply substitutes the variable in the postcondition, sequencing chains the rules, and conditionals merge the two branches. The final condition at the top is exactly what must hold before running the program to guarantee the postcondition holds after.

The predicate transformer rules are beautifully mechanical for straight-line code:

• Assignment $x := e$: replace every occurrence of $x$ in the postcondition $Q$ with $e$. Written $wp(x := e,\; Q) = Q[x \mapsto e]$.
• Sequence $S_1;\; S_2$: chain backward — $wp(S_1;\; S_2,\; Q) = wp(S_1,\; wp(S_2,\; Q))$.
• Conditional $\mathbf{if}\; b\; \mathbf{then}\; S_1\; \mathbf{else}\; S_2$: take the conjunction of both branches — $wp = (b \Rightarrow wp(S_1, Q)) \;\wedge\; (\neg b \Rightarrow wp(S_2, Q))$.

Loops break the mechanical paradise. A loop $\mathbf{while}\; b\; \mathbf{do}\; S$ has no finite formula unless you supply a loop invariant — a condition that holds before, during, and after every iteration. Finding the right invariant is not mechanical: in general it is undecidable, as hard as the halting problem.

This is the deep limit: for any fixed program without loops, the weakest precondition is computable in linear time. Add a loop and you need a human insight — or a very clever search — to close the proof.

The predicate transformer appears wherever software must be proven correct, not just tested:

• Deductive verifiers (Dafny, Frama-C, VeriFast): you annotate code with pre/postconditions and invariants; the tool runs the wp calculus and hands the resulting formulas to an SMT solver.
• Hoare logic: Dijkstra's wp is the semantic foundation of Hoare triples $\{P\}\; S\; \{Q\}$ — the rule for assignment is exactly the wp substitution.
• Compiler optimizations: a compiler can prove that a branch is dead, a variable is unread, or an array access is in-bounds by computing the weakest precondition of the check and seeing whether it is always true.
• Safety-critical systems: avionics, medical devices, and nuclear control software use wp-based proofs to certify that certain bad states are unreachable.
• Automated test generation: tools like Pex/IntelliTest symbolically execute backward to find inputs that cover every path — this is just the wp computed over a path condition.

Understanding weakest preconditions means understanding program equivalence: two programs are equivalent precisely when their wp transformers agree on every postcondition.

Dijkstra's predicate transformer turns the question "what must be true before this code runs?" into a calculation. For any straight-line program, the answer follows mechanically — substitute, chain, merge — and you hold the exact condition that guarantees your result.

The boundary is loops. There, the mechanical rule hits the wall of undecidability: you need a loop invariant, and no algorithm can find one in general. That limit is not a flaw in the calculus; it is a precise map of what formal reasoning can and cannot automate.

Every time a modern verifier proves your function correct, it is running Dijkstra's rules in the background. The predicate transformer did not just give us a technique — it gave us a language for what program correctness even means.