Introduction

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.

Propagate Backward

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.

<!-- Weakest Precondition demo: propagate a postcondition backward through statements. -->
<p class="hint">Select a program and a postcondition, then press <b>Compute wp</b>. Each step shows Dijkstra's rule applied to one statement — the final box is the weakest precondition.</p>
<div class="controls">
  <label>Program:</label>
  <select id="prog-select">
    <option value="assign1">x := x + 3</option>
    <option value="assign2">y := x * 2</option>
    <option value="seq">x := x + 1 ; y := x * 2  (sequence)</option>
    <option value="cond">if x >= 0 then y := x else y := -x  (conditional)</option>
  </select>
</div>
<div class="controls">
  <label>Postcondition:</label>
  <select id="post-select">
    <option value="pos">y > 0</option>
    <option value="even">y % 2 === 0  (y is even)</option>
    <option value="gt10">y > 10</option>
  </select>
</div>
<div id="steps-area"></div>
<div class="btns">
  <button id="compute-btn" type="button">Compute wp</button>
  <button id="reset-btn" type="button" class="ghost">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; }

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));

// wp(S, Q) = weakest precondition: the most permissive pre-state guaranteeing Q after S.
// wp(x := e, Q) = Q with every free x replaced by e.
// wp(S1;S2, Q) = wp(S1, wp(S2, Q)) — chain backward.
// wp(if b then S1 else S2, Q) = (b => wp(S1,Q)) AND (not b => wp(S2,Q)).

// Available programs keyed by demo option id.
const PROGRAMS = {
  assign1: {
    stmts: [{ type: 'assign', v: 'x', e: 'x + 3' }]
  },
  assign2: {
    stmts: [{ type: 'assign', v: 'y', e: 'x * 2' }]
  },
  seq: {
    stmts: [
      { type: 'assign', v: 'x', e: 'x + 1' },
      { type: 'assign', v: 'y', e: 'x * 2' }
    ]
  },
  cond: {
    stmts: [{ type: 'cond', b: 'x >= 0', s1: { v: 'y', e: 'x' }, s2: { v: 'y', e: '-x' } }]
  }
};

// Available postconditions keyed by demo option id.
const POSTCONDS = {
  pos:  'y > 0',
  even: 'y % 2 === 0',
  gt10: 'y > 10'
};

// Textual substitution: replace all free occurrences of varName with expr.
function substitute(pred, varName, expr) {
  return pred.split(varName).join('(' + expr + ')');
}

// Compute wp for a single statement given postcondition post.
function wp(stmt, post) {
  if (stmt.type === 'assign') {
    return substitute(post, stmt.v, stmt.e);
  }
  if (stmt.type === 'cond') {
    const wp1 = substitute(post, stmt.s1.v, stmt.s1.e);
    const wp2 = substitute(post, stmt.s2.v, stmt.s2.e);
    return '(' + stmt.b + ') ? (' + wp1 + ') : (' + wp2 + ')';
  }
  return post;
}

// Human-readable description of a statement.
function describeStmt(stmt, t) {
  if (stmt.type === 'assign') {
    return i18nFmt('%v% := %e%', { v: stmt.v, e: stmt.e });
  }
  if (stmt.type === 'cond') {
    return i18nFmt('if %b% then ... else ...', { b: stmt.b });
  }
  return '';
}

// Name the Dijkstra rule used for a statement.
function ruleLabel(stmt) {
  if (stmt.type === 'assign') return 'rule: wp(x := e, Q) = Q[x ↦ e]';
  if (stmt.type === 'cond') return 'rule: wp(if b then S1 else S2, Q) = (b ⇒ wp(S1,Q)) ∧ (¬b ⇒ wp(S2,Q))';
  return '';
}

function compute() {
  const progKey = document.getElementById('prog-select').value;
  const postKey = document.getElementById('post-select').value;
  const area = document.getElementById('steps-area');
  area.innerHTML = '';

  const prog = PROGRAMS[progKey];
  const postStart = POSTCONDS[postKey];

  // Backward pass: build the predicate array from postcondition to precondition.
  const stmts = prog.stmts;
  const preds = [postStart]; // preds[0] will hold the final weakest precondition after the loop.
  for (let i = stmts.length - 1; i >= 0; i--) {
    preds.unshift(wp(stmts[i], preds[0]));
  }

  // Render one card per statement showing the rule applied.
  for (let i = 0; i < stmts.length; i++) {
    const stmt = stmts[i];
    const pre = preds[i];
    const post = preds[i + 1];
    const div = document.createElement('div');
    div.className = 'step' + (i === stmts.length - 1 ? ' step-final' : '');
    div.innerHTML =
      '<span class="stmt">' + describeStmt(stmt) + '</span><br>' +
      '<span class="rule">' + ruleLabel(stmt) + '</span><br>' +
      i18nFmt('postcondition: <span class="pred">%pred%</span>', { pred: post }) +
      '<br>' +
      i18nFmt('wp: <span class="pred">%pred%</span>', { pred: pre });
    area.appendChild(div);
  }

  // Add a highlighted card for the overall weakest precondition.
  const finalDiv = document.createElement('div');
  finalDiv.className = 'step step-final';
  finalDiv.innerHTML =
    '<strong>Weakest Precondition:</strong><br>' +
    '<span class="pred">' + preds[0] + '</span>';
  area.appendChild(finalDiv);
}

function resetDemo() {
  document.getElementById('steps-area').innerHTML =
    '<p class="empty-hint">Press "Compute wp" to see the backward propagation.</p>';
}

document.getElementById('compute-btn').addEventListener('click', compute);
document.getElementById('reset-btn').addEventListener('click', resetDemo);
resetDemo();
Result
Console

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 Real Complexity

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

  • Assignment x:=ex := e: replace every occurrence of xx in the postcondition QQ with ee. Written wp(x:=e,  Q)=Q[x↦e]wp(x := e,\; Q) = Q[x \mapsto e].
  • Sequence S1;  S2S_1;\; S_2: chain backward — wp(S1;  S2,  Q)=wp(S1,  wp(S2,  Q))wp(S_1;\; S_2,\; Q) = wp(S_1,\; wp(S_2,\; Q)).
  • Conditional if  b  then  S1  else  S2\mathbf{if}\; b\; \mathbf{then}\; S_1\; \mathbf{else}\; S_2: take the conjunction of both branches — wp=(b⇒wp(S1,Q))  ∧  (¬b⇒wp(S2,Q))wp = (b \Rightarrow wp(S_1, Q)) \;\wedge\; (\neg b \Rightarrow wp(S_2, Q)).

Loops break the mechanical paradise. A loop while  b  do  S\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.

Where It Matters

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}\{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.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/weakest-precondition/Content licensed under CC BY-NC 4.0.