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.
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.The loop checklist (see the iterative command) splits cleanly into two halves. Conditions 1–3 — the invariant is established, preserved, and on exit implies the postcondition — give you everything except the guarantee that the exit is ever reached. A loop can satisfy all three and still spin forever:
# invariant P: s = sum of b[0..i-1] (true throughout)
i := 0 ; s := 0 ;
do i ≠ n →
s := s + b[i]
# forgot i := i + 1 !
od
# P is preserved every iteration, yet i never
# reaches n — the loop runs forever.# bound t: n - i (must be > 0 while looping
# and strictly decrease each pass)
i := 0 ; s := 0 ;
do i ≠ n →
s := s + b[i] ;
i := i + 1 # t = n-i drops by 1 → halts
odSo a bound function is a fresh obligation. For a loop do B → S od with invariant P, discharge:
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.
When one loop sits inside another, a single dimension is not always enough. Two techniques:
Pick one integer expression that strictly decreases on every step of either loop. For a fixed inner range of size W, the expression (outer_remaining) * W + (inner_remaining) works, because completing an inner pass drops the inner term, and each outer step drops the whole product by at least one even as the inner term resets.
# iterate over an m×n matrix
# outer bound: m - r, inner bound: n - c
# combined: t = (m - r) * n + (n - c)
r := 0 ;
do r ≠ m →
c := 0 ;
do c ≠ n →
visit(r, c) ;
c := c + 1 # inner term (n-c) drops → t drops
od ;
r := r + 1 # (m-r) drops; even as c resets, t drops
odEquivalently, use the tuple (m - r, n - c) ordered lexicographically — a genuinely well-founded order on pairs of naturals. The outer step decreases the first component (so the pair decreases regardless of the second); the inner step holds the first fixed and decreases the second. Lexicographic tuples are the clean way to reason about loops whose inner counter resets.
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.| 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. |