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
This deck explains contracts, implication, weakest preconditions, invariants, and termination before using them. The foundations and runnable lab are included here; related decks are optional further reading.
How can a contract determine the loop we should write?
Understand the data, the rule, and the required result. Then run the complete Python program and modify one thing at a time.
No companion presentation is required. Python syntax and any mathematical notation are explained as they are introduced.
What the caller must supply.
What the returned answer must satisfy.
A fact true at each loop boundary.
A lower-bounded measure that strictly decreases.
Trace each step and name what changed. Ask which fact stayed true and what should happen on an empty, invalid, or boundary input.
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 11 — 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 : 0 ≤ i < n : b[i] > 0) # Python: all(b[i] > 0 for i in range(n)) # "some item equals x" (∃ i : 0 ≤ i < n : b[i] == x) # Python: any(b[i] == x for i in range(n))
Read the three parts as: which variable : which values it takes : what must hold.
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 12).
Edge case worth knowing: the sum of nothing is 0, “all of an empty list” is true, “any of an empty list” is false.
Every contract is an “if… then…”. A ⇒ B means: whenever A is true, B is true too. Think of it as a promise.
| rains (A) | umbrella (B) | promise kept? (A ⇒ B) |
|---|---|---|
| yes | yes | kept |
| yes | no | broken — the only way |
| no | yes | kept |
| no | no | kept |
On a dry day you cannot break the promise, whatever you carry. So “false implies anything” is true. Logicians call this vacuously true.
In set terms, A ⇒ B means A's set sits inside B's set. So x > 100 ⇒ x > 0: the stronger condition implies the weaker one.
Two safe moves follow, and you will use both:
x > 0, it works for x > 100.x > 100, it also ends with x > 0.Watch out: a precondition of false makes any contract “true” — it just never applies. Too-strong preconditions look safe and promise nothing.
wp) 30-SECOND RECAPThe calculus models defined operations and normal termination. A mathematical proof depends on its language/arithmetic assumptions; sampled tests do not establish universal correctness.
The 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 GUARDRAILSThe calculus models defined operations and normal termination. A mathematical proof depends on its language/arithmetic assumptions; sampled tests do not establish universal correctness.
You 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.
Use a nonnegative integer variant that strictly decreases on every iteration. The guard may stop while it is still positive; reaching exactly zero is not required.
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. The book splits check 4 into two (“bound > 0 while looping” and “bound drops each pass”), so you will also see “five checks.” 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 and 0 ≤ i ≤ n
Bound: n - i (precondition: n ≥ 0)
| 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 — while looping, i ≤ n and i != n, so n-i > 0. It starts at 4, drops by 1 each pass, hits 0. ✓
Under the stated integer precondition, the invariant and decreasing variant prove correctness and termination. Tests remain useful for checking that the implementation matches the derivation.
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, the first one
Goal: x not in b[0..i-1] and b[i] == x.
Invariant (drop a part): drop b[i] == x, keep “x hasn't appeared in b[0..i-1].” The dropped part becomes the stop test.
Bound: n - i. It stays positive only because x is still ahead (the promise).
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
# now: i == n means "not found"
The goal changes too: i == n (x is nowhere) or b[i] == x. The index test goes first, so b[n] is never read. You didn't need a crash to find the out-of-range read — the reasoning surfaced it up front.
Find the biggest value in b[0..n-1]. Follow the recipe: promise, invariant, then start, stop test, body.
# promise: # given n ≥ 1 # ensure m == max of b[0..n-1]
1 Invariant = replace the constant n with a variable i:m == max of b[0..i-1] and 1 ≤ i ≤ n
2 Stop test: invariant + i == n is the promise, so loop while i != n.
3 Start: the smallest easy case is one item. m = b[0]; i = 1. This is where n ≥ 1 matters: an empty list has no max.
4 Body: to grow the range by one, the new max is the larger of m and b[i].
5 Bound: n - i.
# {n ≥ 1}
m = b[0]; i = 1
while i != n:
if b[i] > m:
m = b[i]
i = i + 1
# {m == max of b[0..n-1]}
Trace b = [3, 9, 2, 9, 5]:
| i | b[i] | m after | max of b[0..i] |
|---|---|---|---|
| start | — | 3 | 3 |
| 1 | 9 | 9 | 9 |
| 2 | 2 | 9 | 9 |
| 3 | 9 | 9 | 9 |
| 4 | 5 | 9 | 9 |
The last two columns always match: that is the invariant, visible. > or ≥ both work here. If you also want the index of the first max, > is the one that keeps it.
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
# N = the starting n (n ≥ 0)
# invariant: acc * fac(n) == fac(N)
# bound: n
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).
Then the “invariant” just describes the code, bugs and all. Write it from the goal, before the loop body exists.
i ≥ 0 holds every pass, but check 3 fails: it says nothing about the answer. A good invariant mentions the result variable.
In the sum loop, right after i = i + 1 and before s = s + i, the invariant is false. That is fine. It only has to hold at the top of each pass.
Sum of nothing is 0. Max of nothing does not exist, so it needs n ≥ 1. If “start true” fails for an empty list, you need a precondition.
Stronger = smaller set = more demanding. x > 100 is stronger than x > 0. “Weakest precondition” = the least demanding one.
Tests check the inputs you tried. The four checks cover every input that meets the precondition. Use tests to catch slips in the proof, not instead of it.
Six short questions. Work each on paper, then click “Answer.”
Which is stronger: x > 5 or x > 3?
x > 5. It allows fewer values, and x > 5 ⇒ x > 3.
True or false: (1 == 2) ⇒ (5 < 0)?
True. The “if” part is false, so the promise cannot be broken.
“Every item of b[0..n-1] is even.”
(∀ i : 0 ≤ i < n : b[i] % 2 == 0), or in Python all(v % 2 == 0 for v in b).
c, i = 0, 0
while i != n:
if b[i] == x: c = c + 1
i = i + 1
# goal: c == how many x in b
c == how many x in b[0..i-1], and 0 ≤ i ≤ n. Bound n - i.
b > 0?In the division example (Example B), what goes wrong if b == 0?
r = r - 0 never shrinks, so the bound r stalls and the loop runs forever. Check 4 fails. That is why the promise needs b > 0.
Is n a valid bound for while n > 1: n = n // 2?
Yes. While looping n > 1 > 0, and n // 2 < n for every n ≥ 1. It even ends fast: about log2 n passes.
| Predicate | A true/false statement about the program's state, like x > 0. Also a set of states. |
| Stronger / weaker | A is stronger if A ⇒ B: smaller set, more demanding. |
| Quantifier | ∀ (“for all”) and ∃ (“there exists”). Python's all and any. |
| Specification | The pair precondition + postcondition. The promise the code makes. |
| wp(S, R) | Weakest precondition: the least demanding start state from which S surely ends in R. |
| Derivation | Building code step by step from its spec, so each line has a reason. |
| Invariant | A fact true at the top of every loop pass. |
| Bound function | A whole number that is > 0 while looping and drops each pass. |
| Weakening R | The four ways to get an invariant from the goal: drop a part, constant → variable, widen a range, keep both. |
| Contract | A function's spec. Callers rely on it instead of reading the body. |
| Frame | The list of things a function is allowed to change. |
| Aliasing | Two names for the same variable or object, which breaks naive reasoning. |
| 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
How can a contract determine the loop we should write?
The file contains its own imports, data generator or fixture, implementation, and checks.
python3 -m venv .venv source .venv/bin/activate # No third-party packages required python science_of_programming.py python science_of_programming.py --self-test
Use Python 3.10+. On Windows, activate with .venv\Scripts\Activate.ps1. Required packages: Python standard library.
Read the contract first. Identify the inputs, intermediate state, and return value in this excerpt from the verified file.
def divide(a: int, b: int) -> tuple[int, int]:
"""Pre: a>=0, b>0, both integers. Post: a=q*b+r and 0<=r<b."""
if not isinstance(a, int) or not isinstance(b, int) or a < 0 or b <= 0:
raise ValueError("a must be a nonnegative integer and b a positive integer")
q, r = 0, a
# Invariant: a == q*b + r and r >= 0. Bound: r.
while r >= b:
q, r = q + 1, r - b
return q, rdivide(17,5): (3, 2) divide(0,5): (0, 0) first_index([4,8,8],8): 1 first_index([4,8,8],7): 3
Output was captured from the complete program running in an isolated temporary directory. Floating-point digits and compressed sizes may vary across versions/hardware.
660 checks passed, including boundary cases and independent reference comparisons where applicable. These executed checks complement the reasoning; they are not a universal proof.
Modify division to record every (q,r) pair. Verify the conservation equation and decreasing remainder at each step.
The invariant is a=q*b+r with r≥0. Each step adds 1 to q and subtracts b from r. Positive b makes r strictly decrease.