David Gries' classic, in plain English.
The big idea: write the program and its proof together — so it's right the first time, not “right once the tests pass.”
Say exactly what's true before and after
From the goal to the start (that's wp)
Name what stays true each pass
Same method for big & hard programs
New to wp? Watch the companion deck first: /presentations/weakest-preconditions.html. Full chapter notes at /sop/.
Normal habit: write code, run it, patch what breaks. Gries flips it: start from what the code must promise, and let that build the code.
def divide(a, b): q, r = 0, a while r >= b: r -= b q += 1 return q, r # does it work for a=0? b>a? # negatives? you find out when # a test fails (if you wrote one)
Tests can show bugs exist — never that they're all gone.
# promise: # given a ≥ 0 and b > 0 # ensure a = q*b + r and 0 ≤ r < b # # from that promise, the loop's # start, test, and body are FORCED # (we derive the whole thing on # slide 10 — nothing is guessed)
“Develop the program and its proof hand in hand, proof leading.”
Everything rests on one simple picture. A condition like x > 0 just names all the situations where it's true. That's it.
x > 0 = every situation where x is positive.true = all situations (no restriction).false = no situation (impossible).x > 0 and y > 0 = situations in both sets (overlap).Stronger = fewer situations, more demanding (x > 100). Weaker = more situations, more relaxed (x > 0).
“Weakest” = the most relaxed condition that still does the job. That word runs through the whole book.
To talk about arrays you need two everyday words: “all of them” and “at least one.” That's all the fancy symbols mean.
# "every item is positive" ∀ i : all(b[i] > 0) # reads: for-all i, b[i] > 0 # "some item equals x" ∃ i : any(b[i] == x) # reads: there-exists i, b[i]==x
Same idea as Python's all(...) and any(...).
Adding one more item to a sum or a check:
sum of b[0..i] = sum of b[0..i-1] + b[i]
“Total so far, plus the next one.” This tiny fact is exactly what a loop body does each pass — it's how invariants grow (slide 8).
Edge case worth knowing: the sum of nothing is 0, “all of an empty list” is true, “any of an empty list” is false.
wp) 30-SECOND RECAPThe book's core tool. wp(code, goal) = “what must be true before, so the goal holds after?” You compute it by reading code backwards.
# goal: x > 5 x = x + 1 # replace x with x+1 → x > 4
Copy the goal, swap in the new value.
x = x + 1 y = x * 2 # goal: y > 10 → x > 5 → x > 4
Push the goal up, last line first.
if x≥0: r = x else: r = -x # goal: r = |x| → true (both ok)
Every branch must reach the goal.
“Weakest” means the answer is the most relaxed input rule that still works — and guaranteed includes “the code actually finishes.” Full walkthrough in the Weakest Preconditions deck.
wp Always Respects GUARDRAILSYou don't memorize these to use the method — they're just why it never misbehaves.
Code can't make the impossible happen.
wp(code, false) = false — nothing gets you to an impossible goal.
An easier goal never demands a stricter input.
Weaken the goal → the required before-condition weakens too.
Want A and B? Solve for A, solve for B, combine.
wp(S, A and B) = wp(S,A) and wp(S,B)
If a rule you wrote ever broke one of these, the rule would be wrong. They're the sanity checks that keep the whole system trustworthy.
You can't read backwards through a loop (how many times does it run?). So you describe it with two invented things and check a short list.
A fact that's true every pass — your progress-so-far statement.
When the loop ends, invariant + “loop finished” must add up to your goal.
A number that counts down to 0 — positive while looping, smaller each pass.
Can't shrink below zero forever ⇒ the loop must stop.
1 starts true · 2 stays true · 3 gives the goal on exit · 4 the bound shrinks to 0
1–3 are the invariant's job; 4 is the bound's job. We apply this on the next slides.
The invariant is the creative part. Gries' recipe: take your goal and relax it so it's easy to make true at the start — then let the loop drive it to the full goal.
Goals often look like “answer is computed AND we've handled everything.”
Keep the first part as the invariant. Turn “handled everything” into the reason the loop stops.
# goal: sum done AND i has reached n # invariant: sum done (for 0..i) ← keep # loop until: i == n ← drop→stop
| Drop a part | keep one half of an “A and B” goal; the other half becomes the stop test |
| Constant → variable | replace a fixed n with a growing counter i |
| Widen a range | let a value roam over a bigger area, shrinking it each step (search) |
| Keep both true | combine the parts of the before/after that must always hold |
“Drop a part” covers most loops you'll ever write.
i = 0; s = 0 while i != n: i = i + 1 s = s + i # goal: s == 1+2+...+n
Invariant (drop-a-part): s == 1+..+i
Bound: n - i
| pass | i | s | 1+..+i | bound |
|---|---|---|---|---|
| start | 0 | 0 | 0 | 4 |
| 1 | 1 | 1 | 1 | 3 |
| 2 | 2 | 3 | 3 | 2 |
| 3 | 3 | 6 | 6 | 1 |
| 4 | 4 | 10 | 10 | 0 |
1 Starts true — i=0, s=0: sum of nothing is 0. ✓
2 Stays true — each pass adds the next i to s; “s = 1..i” still holds (see the two matching columns). ✓
3 Gives the goal — loop ends at i=n; invariant becomes s = 1..n. ✓
4 It ends — bound n-i starts at 4, drops by 1 each pass, hits 0. ✓
Four ticks → correct and terminating, for every n ≥ 0. No test run needed.
Divide a by b using only subtraction. Watch the code appear from the invariant — nothing is guessed.
# promise: # given a ≥ 0, b > 0 # ensure a = q*b + r and 0 ≤ r < b
1 Invariant = drop the hard part (r < b):a = q*b + r and 0 ≤ r
2 Stop test = the dropped part: loop while r ≥ b.
3 Start so the invariant is trivially true: q=0, r=a → a = 0·b + a. ✓
4 Body = whatever keeps the invariant while shrinking r: move one b from r into q.
# {a ≥ 0 and b > 0} q = 0; r = a while r >= b: r = r - b q = q + 1 # {a = q*b + r and 0 ≤ r < b}
# (q+1)*b + (r-b) # = q*b + r = a ← invariant kept # r-b ≥ 0 (since r ≥ b) ← still valid # r got smaller ← bound shrinks
Every line was forced by the promise + invariant.
Find the first spot where b[i] == x. This shows how skipping a precondition shows up as a broken proof — the reasoning does your QA.
# promise: x is somewhere in b i = 0 while b[i] != x: i = i + 1 # found it: b[i] == x
Invariant (widen the range): “x hasn't appeared in b[0..i-1], and is still somewhere from i on.”
Bound: n - i.
If x is not in b, the invariant's “still somewhere from i on” becomes false, and nothing stops i running off the end of the array.
The proof tells you the exact fix: add a bounds check to the test —
while i < n and b[i] != x: i = i + 1
You didn't need a crash to discover the off-by-one — the reasoning surfaced it up front.
Every derivation ends in little logic steps like “this implies that.” Bugs love to hide in a hand-wavy “obviously.” So the book gives exact rules for each step.
1 P and Q (given) 2 P (from 1: "and" → each part) 3 Q (from 1: same) 4 Q and P (from 3,2: combine)
Each connective (and, or, implies, not, for-all, exists) has a rule to build it and a rule to use it. No leaps.
assume A ... do some steps ... reach B ⇒ therefore A implies B
Exactly how you argue informally — “suppose the input is valid… then the output is right” — just written so a machine could check it.
This is the ancestor of today's proof assistants (Coq, Lean, Isabelle). Day to day you use algebra; these rules are the bedrock underneath.
Prove a function correct once against its own promise. Every caller just trusts the contract — nobody re-reads the body. That's how proofs (and code) stay manageable.
def inc(n): # given n ≥ 0 # ensure result == n + 1 return n + 1 # at a call: fill in the actual value m = inc(k) # if k ≥ 0, then m == k + 1 — done
The caller reasons from the contract, not the code.
Payoff: proofs snap together like the functions do. A verified function is a trustworthy building block.
A whole number that keeps getting strictly smaller and never goes below 0 cannot do so forever. Eventually it hits bottom — and the loop stops.
“Correct” and “stops” are separate promises: a loop can compute the right thing yet spin forever. The bound is what closes that gap.
(outer, inner) compared like a clock: outer ticks down, or outer stays and inner ticks down. Still always “going down.”n - i, the remaining r, the size of the unprocessed part.Read a recursive definition as an invariant over a running total, and it becomes a loop.
# factorial, recursive def fac(n): return 1 if n==0 else n*fac(n-1) # same thing, as a loop acc = 1 while n != 0: acc = acc * n n = n - 1 # invariant: acc * fac(n) = original!
Keep an extra variable, kept true by the invariant, so you stop recomputing from scratch.
# slow: re-add b[0..i] every pass → O(n²) for i in range(n): s = sum(b[0:i+1]) # fast: carry the running total → O(n) s = 0 for i in range(n): s = s + b[i] # invariant: s = sum so far
Same proof shape, one added fact — a re-scan becomes a single update.
The famous Dutch National Flag (sort an array of 3 colors in one pass) is “just” a clever invariant over a few regions plus a shrinking bound. Three lines or three hundred — state, invariant, bound.
Some programs can be un-run — step the assignments in reverse to recover the input. A neat reminder that programs are math objects you can transform, not just execute.
The best comments are assertions: the promise at the top, and the invariant at each loop. The smallest text that lets the next reader rebuild your reasoning.
Lineage: Floyd (asserts on flowcharts) → Hoare (the {before} code {after} triple) → Dijkstra (wp + guarded commands) → Gries (turned it into something teachable).
| Situation | What to do |
|---|---|
x = e | goal with x replaced by e |
| lines in a row | work backwards, last line first |
if / else | every branch must reach the goal |
| a loop | invariant + bound, 4 checks |
| a function | prove once, call by its contract |
1 starts true · 2 stays true · 3 gives the goal · 4 it ends.
Get the invariant right and the start, the test, the body, and the “why it stops” all follow almost by themselves.
Weakest Preconditions deck · the 16 chapter notes · loops & invariants