← CatZep/Engineering Guides/The Science of Programming
An invariant proves a loop does the right thing if it stops. The bound function is the separate, equally essential argument that it actually stops — and it rests on one elegant idea from mathematics: well-founded sets.
Student edition · understand, apply, verify
Choose genuinely decreasing measures and recognize invalid termination examples.
What you should be able to do: Use natural-number or lexicographic progress and distinguish per-loop proof boundaries from arbitrary internal steps.
Assumes basic programming, not formal-methods notation. This guide defines the needed notation locally. Scalar proofs use mathematical integers unless stated otherwise; finite arrays require integer valid bounds. Guarded-command notation is not Python syntax. Machine overflow, floats, exceptions, aliasing, and concurrency need additional contracts.
In Gries’ framework a loop is proven totally correct by two independent inventions of the programmer: the invariant P, which captures what is always true, and the bound function t, which captures how much work is left. The invariant gives you partial correctness — “if the loop terminates, the result is right.” Only the bound function closes the gap to total correctness by guaranteeing the loop cannot run forever. This page is about that second half: what a bound function is, why it works, how to choose one, and the traps that make a plausible-looking bound wrong.
{P} S {Q} for a Hoare triple, guarded commands (do…od) for loops, t for the bound (variant) function. See the book for the full treatment.Read these definitions first, or use the linked terms as you go. The examples and limitations are local to this guide; companion pages are optional.
A variant strictly decreases each iteration in a well-founded order. A natural-number variant cannot decrease forever while remaining nonnegative.
Example. An array scan uses n−i; repeated subtraction division uses remaining dividend.
Boundary. A positive real can halve forever. Use discrete domains or another well-founded order; nested loops need a correct combined or lexicographic bound.
A predicate true after initialization and after each iteration. Together with the false exit guard it establishes the required result.
Example. While summing, preserve 0≤i≤n and s=sum(b[0:i]); add b[i] then advance i.
Boundary. An invariant alone does not prove termination. Validate array/domain bounds and establish the invariant before iteration.
∀ means every value in a domain satisfies a property; ∃ means at least one does. P⇒Q says every P-state is a Q-state, so P is stronger.
Example. ∀i in 0≤i Boundary. Negation switches ∀/∃ and negates the predicate. Preserve domains and do not reverse implication.
Big-O describes growth with input size under a cost model. Worst-case, expected, amortized, and output-sensitive bounds are distinct promises.
Example. Binary search is O(log n) comparisons on sorted random-access input; printing every subset needs exponential output work.
Boundary. Expected hash-table O(1) is not worst-case O(1). Include output size, recursion space, input assumptions, integer costs, and library operations.
Partial correctness does not imply termination. A valid no-progress example must genuinely preserve its invariant. If i=0,s=0 and P says s=sum(b[0:i]), a skip body preserves P while i never reaches positive n. Repeatedly adding b[0] with i fixed generally violates P; that is not an invariant-preserving example.
# Integer n>0; P: i=0 and s=0=sum(b[0:0]).
i := 0; s := 0
while i != n:
skip # P preserved, but n-i never decreases.
# No total-correctness guarantee.For a finite scan, validate integer 0≤n≤len(b), maintain the prefix invariant, and decrease n−i each iteration. Termination arguments also assume body operations terminate; a blocking external call is not covered by array-index progress alone.
Why does “a positive integer that strictly decreases” force termination? Because of a property of the integers called well-foundedness.
x0 > x1 > x2 > …The natural numbers under < are the canonical well-founded set: you cannot keep subtracting and stay ≥ 0 forever. Each loop iteration maps the machine state to a value of t in {0, 1, 2, …}; condition 5 says consecutive values form a strictly decreasing chain, and condition 4 says they never drop below the floor. In a well-founded set a strictly decreasing chain must be finite — therefore the loop executes only finitely many times. That is the entire termination argument, and it is why an integer bound bounded below by 0 is all you ever need.
The idea generalises: t need not be an integer — any expression valued in a well-founded set works (lexicographically ordered tuples, for instance, used below for nested loops). Integers just happen to be the most convenient choice.
A good bound function measures how much work is left to do. It does not have to equal the exact number of remaining iterations — it only has to be a value in a well-founded set that stays non-negative and strictly decreases. That freedom makes bounds easy to find:
| Loop | Natural bound t | Why it works |
|---|---|---|
Scan an array, index i up to n | n - i | Starts at n, drops by 1 each step, hits 0 at exit. |
Integer division by subtraction (r ≥ b) | r | Each pass does r := r - b with b > 0. |
Shrink an interval [lo, hi] | hi - lo | Every step narrows the interval. |
| Process a worklist / stack | number of items remaining | Each step removes at least one (and adds boundedly fewer). |
Euclid’s gcd (x ≠ y) | x + y | Each pass subtracts the smaller from the larger. |
Heuristic: look at the guard. The bound is usually a simple function of the same variables the guard tests, arranged so the guard becoming false coincides with t reaching its floor.
The simplest proof treats nested loops separately: inner variant n−c and outer variant m−r, with nonnegative integer dimensions and terminating body operations. A lexicographic pair works at the appropriate state transitions: row advances decrease the first component even when the column resets.
The combined expression (m−r)×n+(n−c) can tie across the row-advance-plus-reset transition: dropping n and adding n cancels. A discrete transition model can instead use (m−r)×(n+1)+(n−c), where processing a cell decreases one and advancing/resetting a row decreases one. Do not claim a measure decreases at every arbitrary initialization/control statement.
# At row/cell transition boundaries:
t = (m-r) * (n+1) + (n-c)
# A cell advances c: delta t = -1.
# A completed row advances r and resets c from n to 0:
# delta t = -(n+1)+n = -1.State the observation boundaries. For actual nested source loops, proving each loop independently avoids misleading universal per-statement bounds.
Sometimes no single variable moves monotonically, yet a function of the state does. These are where the “measure the remaining work” instinct pays off.
Neither x nor y decreases every step — only one of them changes each time — but their sum always shrinks.
# pre: x > 0 and y > 0 ; bound t: x + y
do x ≠ y →
if x > y → x := x - y
[] y > x → y := y - x
fi
od
# whichever branch runs, x+y strictly decreases
# by the smaller value (> 0), and stays > 0 while x≠y.The indices lo and hi move toward each other by variable amounts, but the interval width hi - lo at least halves — strictly decreasing and bounded below by 0, so the loop runs in O(log n) steps.
# bound t: hi - lo (roughly halves each pass)
do lo < hi →
mid := (lo + hi) / 2 ;
if b[mid] < x → lo := mid + 1
[] b[mid] ≥ x → hi := mid
fi
od| Mistake | Why it breaks the proof |
|---|---|
| Bound can go negative | Violates condition 4 (t > 0 while looping). A bound that dips below 0 no longer lives in the well-founded set, so the finiteness argument collapses. |
| Bound decreases only sometimes | Condition 5 requires a strict decrease on every iteration. A branch that leaves t unchanged permits an infinite run through that branch. |
| Decreases but is not bounded below | An always-decreasing quantity over, say, all integers (no floor) is not well-founded — it can decrease forever. You need both a strict decrease and a floor. |
| Off-by-one at the last iteration | P ∧ B ⇒ t > 0 must hold on the final pass too. A bound that is 0 while the guard is still true (e.g. t = n - i with guard i ≤ n) fails condition 4. |
Using ≤ instead of < | A non-strict “decrease” allows t to stall at the same value indefinitely. The decrease must be strict. |
| Confusing bound with iteration count | Harmless but wasteful: the bound need only dominate the remaining steps, not count them. Insisting on the exact count makes bounds harder to find than they need to be. |
Only loops (and recursion) can fail to terminate, so only they need a variant. The rest compose trivially:
S1 ; S2: terminates if S1 terminates and, from every state S1 can leave it in, S2 terminates.Work through the state changes and the exact claim being checked.
| Step | Evidence, decision, and expected result |
|---|---|
| Track inner work | For a row width n, inner remaining n−c decreases each cell. |
| Track outer work | m−r decreases after an entire row; prove inner termination separately. |
| Avoid a canceling combined measure | (m−r)×n+(n−c) can be unchanged when r advances and c resets. Use a documented transition measure with weight n+1 or lexicographic row/column order. |
| Reject real-number 'progress' | A positive real halving forever is decreasing but not a natural-number termination proof. |
Generally no. A no-progress invariant example should use skip (or another body that actually preserves the predicate).
Download guide_labs.py. Python 3.10+, standard library only. In its directory, run:
python3 guide_labs.py termination
python3 guide_labs.py testThe complete standard-library lab checks the stated finite cases and boundary inputs. Its invariants explain the reasoning; tests alone do not prove all possible inputs.
The program tests its stated finite contracts. It is an educational model, not an implementation of the named production product or a proof of unmodeled distributed faults.
| Idea | The one-line takeaway |
|---|---|
| Two halves of a proof | Invariant ⇒ partial correctness; bound function ⇒ termination. You need both for total correctness. |
| The bound obligation | P ∧ B ⇒ t > 0, and every iteration strictly decreases t. |
| Why it works | A strictly decreasing chain in a well-founded set (like the naturals) must be finite. |
| Choosing one | Measure the work left; it need only dominate the remaining steps, not count them. |
| Nested loops | Use a combined outer*W + inner bound or a lexicographic tuple. |
| Non-obvious bounds | When no variable is monotone, a function of the state often is (x+y for gcd, hi-lo for binary search). |
| Traps | Negative bound, non-strict or occasional decrease, no floor, off-by-one on the last pass. |