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)⌋ + 1 = 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 [0, 1], 1: returns 0, should be 1. |
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 claims the last element is >= x before anyone checked. Then check 5 fails too: the guard allows hi - lo == 0, where hi = mid moves nothing. Hangs on [1], 0. |
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: ZeroDivisionError. And with no stated precondition, bad k gives silent nonsense: k = -1 on [1,2,3] returns [-3.0, -0.0, -0.0, -0.0, -0.0], and k > len(a) returns []. 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: out is a sorted copy of the input # AND unsorted is empty # INV : out + unsorted is a permutation of the # input, out is sorted, and # max(out) <= min(unsorted) 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.
# pre : a > 0 and b > 0 # 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.
for Loops and while True Have Invariants Too MOST PYTHON LOOPSMost Python loops are for loops, not while. The method still applies. The invariant is a fact true at the top of every pass, and the bound is usually built in.
for loop, with its invariantdef count_less(a: list[int], x: int) -> int: """post: returns how many v in a have v < x""" c = 0 for i in range(len(a)): # INV (top of pass i): c == #{v in a[:i] : v < x} if a[i] < x: c += 1 # after the loop: INV with a[:len(a)], i.e. the post return c
| Init | c = 0 and a[:0] is empty — INV holds for free. |
| Bound | Built in: range is finite, and you cannot change it from inside. |
| Exit | All passes done = INV over all of a = the post. |
for i in range(n): ... print(i) # n - 1, not n. And NameError if n == 0!
In a while loop the counter ends at n. In a for loop it ends one short. Do not reuse i after the loop; state the result in its own variable.
while True + break: find the hidden guardwhile True: line = f.readline() if not line: # the real guard, negated break handle(line) # INV : every line before the file position was handled # BOUND: bytes left in the file
The guard is “not at end of file”. Write it down. Every break is a way of stopping, so check 2 must hold at each one.
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) colors = st.lists(st.sampled_from([0, 1, 2])) # = the pre @given(colors) def test_sort_012_matches_sorted(a): assert sort_012(list(a)) == sorted(a)
Two traps avoided. st.integers() would break the precondition (only 0, 1, 2 allowed). And sort_012 sorts in place, so a test like sort_012(sort_012(a)) == sort_012(a) compares a with itself and always passes. Copy first.
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 default 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 about 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) (pre: no cycle) 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.
The reasoning is language-free, but Python has a few habits that quietly change what the code means. Each one below was run; the outputs are real.
xs = [1, 2, 2, 3] for x in xs: if x % 2 == 0: xs.remove(x) # xs == [1, 2, 3] <- a 2 survived
The loop's hidden index skips the item after each removal. Build a new list: [x for x in xs if x % 2].
!=x = 0.0 while x != 1.0: x += 0.1 # after 10 steps x == 0.9999999999999999 # never equals 1.0 -> runs forever
Floats are not exact, so no bound reaches its stop value. Loop over an integer count instead, and compute x = k / 10.
assert (lo <= hi, "bad range") # a non-empty tuple is always truthy assert lo <= hi, "bad range" # right
Python warns (SyntaxWarning) but still runs it. Your invariant check silently checks nothing.
python -O deletes every assert. Use asserts for invariants (your own promises). Use if ...: raise ValueError for preconditions at a public API (slide 12). And never put side effects inside an assert.
In most languages a[-1] crashes. In Python it quietly reads the last item. So a loop that steps one too far to the left gives a wrong answer, not an error. Check 0 must say 0 <= i, not just i < len(a).
mid = (lo + hi) // 2 cannot overflow: Python ints grow as needed. In Java or C, write lo + (hi - lo) / 2. That overflow bug sat in the JDK's binary search for about nine years (fixed 2006).
Six exercises in the order of the recipe. Write your answer, then click to compare.
i, j = 0, len(a) - 1 while i < j: a[i], a[j] = a[j], a[i] i += 1; j -= 1
a[:i] and a[j+1:] already hold their reversed values. a[i:j+1] is untouched. Bound: j - i + 1 (drops by 2).
lo, hi = 0, len(a) - 1 while lo < hi: mid = (lo + hi) // 2 if a[mid] < x: lo = mid + 1 else: hi = mid return lo
Check 1: init does not make a[hi:] >= x true. For [1, 2], x = 5 it returns 1; the answer is 2.
Test max_subarray (slide 14) against its postcondition with Hypothesis.
@given(st.lists(st.integers(), min_size=1)) def test_max_sub(a): n = len(a) assert max_subarray(a) == max( sum(a[p:q]) for p in range(n) for q in range(p+1, n+1))
min_size=1 is the precondition.
# pre: x >= 0 and y >= 0 while y != 0: x, y = y, x % y
y. It is > 0 while looping, and 0 <= x % y < y, so the new y is strictly smaller. (Euclid's gcd.)
while not ok: ok = try_commit()
tries = 0 # BOUND: max_tries - tries while not ok and tries < max_tries: ok = try_commit(); tries += 1 if not ok: raise CommitFailed(tries)
N = n; s = 0 # pre: n >= 0 while n > 0: s += n % 10; n //= 10 # post: s == digit_sum(N)
INV: s + digit_sum(n) == digit_sum(N). Bound: n (or its digit count). Checked by assert on 9075 → 21.
| Precondition (pre) | What the function assumes on entry. Enforced by a guard clause at public APIs. |
| Postcondition (post) | What it promises on return, stated about the result, not the algorithm. |
| Invariant (INV) | True at the top of every loop pass. Written as # INV: and checked with assert. |
| Bound (BOUND) | A non-negative integer that strictly drops each pass. Proves the loop ends. |
| Guard | The loop test B. INV and not B must give the post. |
| Definedness (check 0) | Every expression can run: index in range, divisor not zero, key present, not None. |
| Total correctness | Right answer and always ends. Needs all five checks. |
| Guard clause | An early if bad: raise at the top of a function, so the rest can trust the pre. |
| Sentinel value | A fake “special” return like 0.0 or -1 that hides an error. Avoid. |
| Property-based test | A test that checks a rule for many generated inputs (Hypothesis), not a few examples. |
| Shrinking | Hypothesis cutting a failing input down to the smallest one that still fails. |
| Metamorphic test | Checks a relation between runs (e.g. agrees with bisect) when the answer is hard to compute. |
| Accumulator | An extra parameter that carries the partial result, turning recursion into a loop. |
| Strengthening the INV | Adding a conjunct that remembers work, so the body does less (Kadane). |
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