Gries' method as a working playbook: a spec you can test, a loop you can prove, and a checklist you can run in code review.
Every slide from here is a real function you can paste and run.
Pre and post as Python predicates, not prose
Work backward from the post to the code
Every loop gets one, written down
The number that shrinks — why it stops
Companion decks: the concepts · weakest preconditions · chapter notes at /sop/
Five things you write, in this order. Steps 1–4 are comments and asserts. Step 5 is the code — and by then most of it is forced.
| # | What you write | Where it lives in Python |
|---|---|---|
| 1 | Precondition — what you assume | docstring pre: + a guard clause that raises |
| 2 | Postcondition — what you promise | docstring post: + the property test |
| 3 | Invariant — true before and after every pass | # INV: above the loop + assert inside it |
| 4 | Bound — a non-negative int that strictly shrinks | # BOUND: above the loop |
| 5 | The loop — init, guard, body | falls out of 3 and 4; almost nothing left to guess |
You stop debugging by re-running with different inputs. When something is wrong, one of the five checks on slide 09 fails, and it tells you which line is lying.
def f(a: list[int], x: int) -> int: """One line of what it does. pre : a is sorted ascending post: 0 <= i <= len(a) all(v < x for v in a[:i]) all(v >= x for v in a[i:]) """ if any(a[k] > a[k+1] for k in range(len(a)-1)): raise ValueError("a must be sorted") # pre lo, hi = 0, len(a) # INV: 0 <= lo <= hi <= len(a) # a[:lo] < x and a[hi:] >= x # BOUND: hi - lo while lo < hi: ... return lo
The two comment lines are the design. Delete the body and you could rebuild it from them.
A spec is not a description. It is a predicate — something that is true or false about a concrete state. If you cannot write it as a Python expression, it is not a spec yet.
def insert_pos(a, x): """Find where x goes in the sorted list a."""
Where does a duplicate go — before or after? What if x is bigger than everything? What if a is empty? Three unanswered questions, three future bugs, and no test can tell you which behaviour was intended.
def insert_pos(a: list[int], x: int) -> int: """Leftmost index where x can be inserted. pre : all(a[k] <= a[k+1] for k in range(len(a)-1)) post: 0 <= i <= len(a) all(v < x for v in a[:i]) all(v >= x for v in a[i:]) """
Duplicates: answered (< vs >= splits them left). Empty list: answered (i = 0, both slices empty, both all() vacuously true). Bigger than everything: answered (i = len(a)).
1 What do I assume? → precondition. Anything you assume and do not check is a caller trap.
2 What do I promise? → postcondition. Write it about the return value and the arguments, never about the algorithm.
3 What is the empty / boundary case? → if the postcondition does not answer it, it is under-specified.
wp in Four Lines CHEAT SHEETwp(S, R) = the weakest thing that must be true before statement S so that R is true after. You already do this in your head; these rules make it mechanical.
| Python | wp(S, R) | In words |
|---|---|---|
x = E | R with every x replaced by E | Textual substitution. That is the whole rule. |
S1; S2 | wp(S1, wp(S2, R)) | Push the goal backward through the last line first. |
if B: S1 | (B and wp(S1,R)) or (not B and wp(S2,R)) | Both branches must land in R. |
assert B | B and R | An assert is a demand on the state before it. |
while B: S | invariant + bound | No substitution rule exists. That is why loops need slide 09. |
wp also requires every expression to be defined. wp(y = a[i]/n, R) silently includes 0 <= i < len(a) and n != 0. In Python those two conjuncts are exactly your IndexError and ZeroDivisionError.
# goal after: x == Y and y == X
t = x
x = y
y = t
Push the goal up one line at a time, substituting:
after y = t : x == Y and y == X before : x == Y and t == X ← y:=t before x = y: y == Y and t == X ← x:=y before t = x: y == Y and x == X ← t:=x
The last line says: x and y start as X and Y. Which is true by definition. Proof done, no test run.
# want after i = i + 1: 0 <= i <= n # wp = 0 <= i+1 <= n # = -1 <= i <= n-1 # so before the bump you need i < n
The guard while i < n was not a choice. It is what the arithmetic demanded.
Binary search is famously easy to get wrong (Bentley: 90% of professionals failed to write it correctly). Derived from the postcondition, there is no room to get it wrong.
Post says a[0:i] < x and a[i:len(a)] >= x. Loosen it: let the two known regions grow from nothing instead of meeting at i. Replace i with two variables:
INV: 0 <= lo <= hi <= len(a) all(v < x for v in a[:lo]) all(v >= x for v in a[hi:])
Now read the four pieces straight off the invariant:
| Init | lo, hi = 0, len(a) — both regions empty, so INV holds for free |
| Guard | lo < hi — because INV and lo == hi is the postcondition |
| Bound | hi - lo — the unknown region, non-negative by INV |
| Body | shrink the unknown region without breaking INV |
def insert_pos(a: list[int], x: int) -> int: """pre : a sorted ascending post: a[:i] < x <= a[i:]""" lo, hi = 0, len(a) # INV: a[:lo] < x and a[hi:] >= x # BOUND: hi - lo while lo < hi: mid = (lo + hi) // 2 # lo <= mid < hi if a[mid] < x: lo = mid + 1 # a[:mid+1] < x (sorted) else: hi = mid # a[mid:] >= x (sorted) return lo
Why mid + 1 on one side and plain mid on the other is not a stylistic coin-flip: a[mid] < x means index mid belongs in the left region, so lo must clear it. a[mid] >= x means mid belongs in the right region, so hi must include it.
This is bisect.bisect_left. Derived, not remembered.
a = [1, 3, 3, 7], x = 3| lo | hi | mid | a[mid] | branch | bound |
|---|---|---|---|---|---|
| 0 | 4 | 2 | 3 | >= x → hi = 2 | 4 → 2 |
| 0 | 2 | 1 | 3 | >= x → hi = 1 | 2 → 1 |
| 0 | 1 | 0 | 1 | < x → lo = 1 | 1 → 0 |
| 1 | 1 | — | — | guard false → return 1 | 0 |
The bound column is the termination argument: strictly decreasing, never negative, so at most log2(4) = 2…3 passes. And at exit, a[:1] = [1] < 3 and a[1:] = [3,3,7] >= 3 — the postcondition, verified by reading, not by luck.
| Mutation | Check that fires |
|---|---|
hi = mid - 1 | INV preserved? No. Index mid satisfies a[mid] >= x but is now in neither region — you can skip the answer. Fails on [3], 3. |
lo = mid | Bound decreases? No. When hi == lo+1, mid == lo, so lo does not move. Infinite loop. |
hi = len(a) - 1with while lo <= hi | INV at init? No. a[hi:] now excludes the last element, so the answer len(a) is unreachable. Fails on [1], 5. |
Every one of those is the kind of bug you would normally find by running it and squinting. Here each one has a name and a failing check. You do not need the failing input to know it is broken.
For array algorithms the invariant is a picture. Draw the picture first and the loop writes itself. Task: sort a list of 0s, 1s and 2s in one pass, in place.
lo i hi
v v v
+--------+--------+--------+--------+
| all 0 | all 1 | unknown| all 2 |
+--------+--------+--------+--------+
0 lo i hi len(a)
INV: a[:lo] all 0, a[lo:i] all 1,
a[hi:] all 2, a[i:hi] unknown
and a is a permutation of the input
BOUND: hi - i (unknown region)
Init lo, i, hi = 0, 0, len(a) — everything unknown, three regions empty, INV holds.
Guard i < hi — when i == hi the unknown region is empty and INV is "sorted".
Body look at a[i]; there are only three cases, and each must shrink hi - i.
def sort_012(a: list[int]) -> list[int]: """pre : every v in a is 0, 1 or 2 post: a is sorted and a permutation of the input""" lo, i, hi = 0, 0, len(a) # INV: a[:lo]==0s, a[lo:i]==1s, a[hi:]==2s # BOUND: hi - i while i < hi: if a[i] == 0: a[lo], a[i] = a[i], a[lo] # 1s block shifts right lo += 1; i += 1 # bound -1 elif a[i] == 1: i += 1 # bound -1 else: hi -= 1 # bound -1 a[i], a[hi] = a[hi], a[i] # i does NOT advance return a
Why i does not advance in the last case: the value swapped into position i came from the unknown region, so it is still unknown — the invariant forbids claiming it. That single subtlety is the whole difficulty of this algorithm, and the invariant hands it to you.
Invariants are not just for interview arrays. The loops that page you at 3am — pagination, retries, draining a queue, reconciling two stores — are exactly the loops with an unstated invariant and no bound function.
while not ok: ok = try_commit() # what shrinks? nothing. time.sleep(1) while cursor: rows, cursor = fetch(cursor) sink(rows) # server bug -> same cursor # -> forever, at full QPS
Neither loop has a quantity that is guaranteed to strictly decrease. Correctness of the happy path is not the issue — termination is not guaranteed by anything, so a dependency's bad day becomes your incident.
“What integer does this loop strictly decrease, and what stops it going negative?” If there is no answer, the loop is unbounded — regardless of how correct the body is.
def drain(fetch, sink, *, max_pages: int = 10_000) -> int: """Pull every row from a cursor API into sink. pre : fetch(cursor) -> (rows, next_cursor); next_cursor is None exactly at the end post: every row returned was passed to sink exactly once, and that count is returned raises: BudgetExhausted if the API never ends """ cursor, sent, pages, done = None, 0, 0, False # INV: sent == rows fetched so far == rows given to sink # pages == successful fetch calls so far # done == (last fetch returned cursor None) # BOUND: max_pages - pages while not done and pages < max_pages: rows, cursor = fetch(cursor) pages += 1 # bound -1, always for r in rows: sink(r) sent += len(rows) # INV restored here done = cursor is None if not done: # INV and not-B, but not post raise BudgetExhausted(f"stopped after {pages} pages") return sent
pages += 1 is unconditional on purpose: that is what makes the bound strictly decrease no matter what the server does. The final if exists because the guard has two ways to become false and only one of them implies the postcondition — check 2 on the next slide caught that.
Given a loop with invariant INV, guard B, body S and bound t. Checks 1–3 give the right answer; checks 4–5 give an answer at all. You need all five.
| # | Formally | Say it out loud |
|---|---|---|
| 1 | pre ⇒ INV after init | The setup makes the invariant true — usually by making everything empty. |
| 2 | INV and not B ⇒ post | Stopping for the loop's reason means you are done. Every way of stopping. |
| 3 | INV and B ⇒ wp(S, INV) | One pass leaves the invariant true again. |
| 4 | INV and B ⇒ wp(t' = t; S, t < t') | One pass strictly decreases the bound. Strictly — not "usually". |
| 5 | INV and t <= 0 ⇒ not B | When the bound runs out, the loop is already over. |
Every expression in S must be defined when it runs: no index out of range, no division by zero, no None deref, no missing key. In Python this is where most loop crashes actually live.
def avg_window(a, k): out, i = [], 0 while i <= len(a) - k: out.append(sum(a[i:i+k]) / k) i += 1 return out
Check 0 — k may be 0. Also there is no stated precondition, so k <= 0 silently returns [] for negative k instead of raising. Fix: pre: 1 <= k <= len(a) plus a guard clause.
lo, hi = 0, len(a) while lo < hi: assert 0 <= lo <= hi <= len(a) # INV prev = hi - lo # bound ... assert hi - lo < prev # check 4
Cheap in dev, stripped by python -O. Put them in during derivation, keep the loud ones.
You do not need inspiration. An invariant is the postcondition with one requirement relaxed — so the loop's job is to remove the relaxation. Four standard relaxations cover most loops.
Post is A and B. Keep A as the invariant, make not B the guard.
# post: heap is sorted AND unsorted is empty # INV : the two lists together are a permutation # of the input, and `out` is sorted while unsorted: # not B out.append(pop_min(unsorted))
The workhorse. a[0:n] becomes a[0:i]; the loop grows i from 0 to n.
# post: s == sum(a[0:len(a)]) # INV : s == sum(a[0:i]) and 0 <= i <= len(a) s, i = 0, 0 while i < len(a): s += a[i]; i += 1
Post pins a variable to one value; let it roam over a legal interval instead.
# post: lo == the answer index # INV : the answer is somewhere in [lo, hi) # -> every binary / interval search there is
Keep a relation that both the start state and the end state satisfy.
# post: x == gcd(a, b) # INV : gcd(x, y) == gcd(a, b) and x > 0 and y > 0 # BOUND: x + y x, y = a, b while x != y: if x > y: x -= y else: y -= x return x
Rule of thumb: if the invariant is hard to state, the postcondition is probably wrong or the function is doing two jobs. Split it.
Gries' functions are partial: outside the precondition, nothing is promised. Python has no way to state that — so you enforce it at the boundary and then trust it everywhere inside.
def p95(xs, weights): if xs: if len(xs) == len(weights): if sum(weights) > 0: return _compute(xs, weights) return 0.0 # <- a lie
Three assumptions, all unstated, and a return value that claims “the p95 is zero” when the truth is “you called me wrong.” That 0.0 will land in a dashboard and someone will trust it.
def p95(xs: Sequence[float], weights: Sequence[float]) -> float: """pre : xs non-empty, len(weights) == len(xs), sum(weights) > 0 post: returns the weighted 95th percentile of xs""" if not xs: raise ValueError("xs must be non-empty") if len(weights) != len(xs): raise ValueError( f"len(weights)={len(weights)} != len(xs)={len(xs)}") if sum(weights) <= 0: raise ValueError("weights must sum to a positive value") return _compute(xs, weights) # pre now holds; no ifs left
Validate at the public API. Private helpers assume the precondition — that is what makes them small.
A sentinel makes the caller's postcondition weaker too. The error propagates as a wrong number instead of a stack trace.
The precondition names the quantities; the error message should print them. Free diagnostics.
Example-based tests check the inputs you thought of. The postcondition is a property that must hold for all legal inputs — hand it to Hypothesis and let it hunt.
def test_insert_pos(): assert insert_pos([1,3,5], 3) == 1 assert insert_pos([1,3,5], 0) == 0 assert insert_pos([1,3,5], 9) == 3
Passes. Says nothing about duplicates, the empty list, or lists of length 2 — which is where the off-by-one actually lives.
from hypothesis import given, strategies as st sorted_lists = st.lists(st.integers()).map(sorted) @given(sorted_lists, st.integers()) def test_insert_pos_meets_spec(a, x): i = insert_pos(a, x) assert 0 <= i <= len(a) # post 1 assert all(v < x for v in a[:i]) # post 2 assert all(v >= x for v in a[i:]) # post 3
Three lines, copied out of the docstring. Hypothesis will find the empty list, the duplicate run, and the single-element list on its own — and shrink any failure to the smallest case.
| Tool | What it buys |
|---|---|
assert in the loop | The invariant is checked on every pass in dev and CI, and vanishes under python -O. The cheapest possible proof harness. |
| Hypothesis | Postcondition becomes a universally-quantified test. Failures arrive pre-shrunk to a minimal counterexample. |
icontract / deal | @require / @ensure decorators put pre and post in the signature, enforced at runtime and inherited by subclasses. |
If the postcondition is hard to compute directly, state a relation instead:
@given(sorted_lists, st.integers()) def test_agrees_with_stdlib(a, x): assert insert_pos(a, x) == bisect.bisect_left(a, x) @given(st.lists(st.integers())) def test_sort_is_idempotent(a): assert sort_012(sort_012(a)) == sort_012(a)
The disciplined way to optimise: do not touch the code. Add a conjunct to the invariant that remembers work you are currently redoing, then let the body change to maintain it.
def max_subarray(a: list[int]) -> int: """pre : a is non-empty post: returns max(sum(a[p:q]) for 0 <= p < q <= len(a))""" best, i = a[0], 1 # INV: best == max subarray sum within a[0:i] while i < len(a): # to restore INV we must consider every # subarray ending at i -> a whole inner loop for p in range(i + 1): best = max(best, sum(a[p:i+1])) i += 1 return best
Correct, and the invariant tells you exactly why it is slow: restoring it needs information the loop threw away last pass.
def max_subarray(a: list[int]) -> int: """same spec, same postcondition""" best = end = a[0] i = 1 # INV: best == max subarray sum within a[0:i] # end == max sum of a subarray ENDING at i-1 <- new # BOUND: len(a) - i while i < len(a): end = max(a[i], end + a[i]) # restores conjunct 2 best = max(best, end) # restores conjunct 1 i += 1 return best
Two lines, no inner loop. end is Kadane's algorithm — and it arrives as a consequence of the extra conjunct, not as a trick you had to have seen before.
Slow loop → look at what restoring the invariant costs → add a variable that carries that cost forward → strengthen the invariant to define it → the body shrinks. Running sums, running max, counters, caches, and incremental checkpoints are all this one move.
Python's recursion limit is 1000 and it has no tail-call optimisation, so this conversion is a routine production need. Done by hand it is error-prone. Done by invariant it is bookkeeping.
def length(node) -> int: """post: number of nodes reachable from node""" if node is None: return 0 return 1 + length(node.next)
Not tail recursive — the 1 + happens after the call. RecursionError at 1000 nodes.
def length(node, acc=0) -> int: """post: acc + nodes from node""" if node is None: return acc return length(node.next, acc + 1)
Now tail recursive. The generalised postcondition acc + nodes(node) is already the loop invariant — that is the entire insight.
def length(head) -> int: """post: number of nodes""" node, acc = head, 0 # INV: acc + nodes(node) # == nodes(head) # BOUND: nodes(node) while node is not None: acc += 1 node = node.next return acc
Guard = negated base case. Body = the tail call's arguments, assigned. Return = the base case value.
Guard the negation of the base case.
Body whatever the recursive call passes, written as assignments to the same names.
Bound the same measure that made the recursion terminate — depth, remaining nodes, n.
Not tail recursive and cannot be made so (tree walks, quicksort)? Then the loop needs an explicit stack, and the invariant becomes a statement about the stack contents — e.g. “every node either visited or on the stack, exactly once.”
Every recurring loop bug maps to exactly one missing check. Once you know the map, a bug report tells you where to look before you open the file.
| Symptom in production | Missing check |
|---|---|
| Off by one at the last element | 2 — INV and not B did not actually imply the postcondition |
| Crashes only on empty input | 1 — init did not establish INV for the empty case (or there is no precondition) |
| Hangs / burns CPU forever | 4 — nothing strictly decreases |
| IndexError deep in the loop | 0 — an expression is undefined at the edge of the range |
| Right for singletons, wrong for duplicates | The postcondition was ambiguous about ties |
| Works alone, corrupt under concurrency | INV holds at loop boundaries but is broken mid-body and something else reads it there |
| Retry storm during a dependency outage | 4/5 — no bound, so a broken dependency is an unbounded loop |
> while not done: > done = poll() What integer does this loop strictly decrease, and what keeps it >= 0? If the answer is "none", a slow dependency turns this into an unbounded loop. Suggest a max_polls budget and a raise on exhaustion.
Specific, not stylistic. It names a property the code must have, and there is exactly one way to satisfy it.
An invariant that is only true at loop boundaries is fine single-threaded and lethal shared. Under a lock, the invariant must hold everywhere the lock is released. Writing it down is what makes that question askable.
Full derivation costs ten to twenty minutes per function. Applied everywhere, it is theatre. Applied to the right code, it removes a class of incident.
issued == spent + remaining), it is an invariant and it should be asserted.bisect, itertools, heapq are derived code someone else already proved. Reaching for them is the method.The minimum viable habit: even when you skip everything else, write the # INV: line. It costs one comment and it is the single highest-yield artifact in the whole method.
def f(args) -> T: """<one line> pre : <what I assume, as a Python predicate> post: <what I promise about the return value> """ if not <pre>: raise ValueError(<with the values>) <init: make the invariant true, usually by emptiness> # INV: <post with one thing relaxed> # BOUND: <non-negative int that strictly shrinks> while <the relaxation is not yet removed>: <shrink the bound, restore the invariant> return <INV and not B, which is post>
1 delete a conjunct 2 constant → variable 3 widen a variable's range 4 keep a relation between pre and post
Plus check 0: every expression is defined — index in range, divisor non-zero, key present.
Before writing any loop, finish this sentence: “Every time I get back to the top of this loop, ___ is true, and ___ is smaller than it was.”
If you cannot finish it, you do not yet know what the loop does — and no amount of running it will tell you.
Next: the concepts deck · weakest preconditions · chapter notes on loops