The half of correctness the invariant cannot give you
In the last three guides you learned to argue that an answer is right: a loop invariant survives every iteration, and when the loop stops the invariant plus the exit condition pin down the correct output. Read that sentence again, because it hides a loophole the size of a barn: when the loop stops. The invariant promises nothing about whether the loop ever stops at all. A loop that spins forever never reaches its termination step, so it never delivers a wrong answer — but it never delivers any answer either.
This is exactly the gap between two flavors of correctness you met earlier. Partial correctness says: if the program halts, the answer is right. Total correctness says: the program halts and the answer is right. The invariant buys you partial correctness. To upgrade to total correctness you must separately, explicitly prove termination. The good news: there is essentially one tool for the whole job, and it is beautifully simple.
The decreasing measure, and why it works
Here is the whole idea in one sentence. To prove a loop terminates, attach to it a quantity — call it the measure or variant — and show two things: every iteration makes the measure strictly smaller, and the measure cannot drop below some floor. A value that strictly decreases yet can never go below zero (and only takes whole-number steps) cannot keep decreasing forever; it must hit the floor in finitely many steps, and the loop is forced to stop.
The classic measure is a non-negative integer. Think of it as the number of stairs left below you: each step takes you strictly down at least one stair, and there is a ground floor. You may not know exactly how many steps remain, but you know it is finite, because you cannot descend a finite staircase forever. That picture — strict descent toward an unbreakable floor — is the entire engine. We call any such quantity a well-founded measure, 'well-founded' being the precise word for an ordering with no infinite descending chain.
A worked micro-proof: Euclid's gcd
Let us prove termination of the oldest non-trivial algorithm we have, Euclid's method for the greatest common divisor. Its partial correctness rests on the fact that gcd(a, b) = gcd(b, a mod b); that piece is the gcd correctness proof and we take it as given here. What we want now is the other half: this loop always finishes.
GCD(a, b): // assume a >= 0, b >= 0
while b != 0:
(a, b) = (b, a mod b) // remainder: 0 <= a mod b < b
return a- Choose the measure. Let the measure be b itself, the second variable. Since the loop runs only while b is not 0, and b is a remainder, b is always a non-negative integer — so it has a floor at 0.
- Show it strictly decreases. One pass replaces (a, b) with (b, a mod b). The new value of b is a mod b, the remainder of a divided by b. By the definition of remainder, 0 <= a mod b < b. So the new b is strictly less than the old b. Strict descent: confirmed.
- Apply the principle. We have a non-negative integer that strictly decreases each iteration. It cannot do so more than (starting value of b) times before reaching 0. When b reaches 0 the while-condition fails and the loop exits. Therefore GCD terminates on every valid input.
Notice how cheap that was. We did not need to know how many iterations run — a separate, harder question whose answer happens to be O(log of the smaller input). Termination only needs the direction of motion plus a floor, never the exact distance. That is the recurring relief of this technique: proving a loop ends is almost always far easier than counting how long it takes.
Measures beyond a single integer
Not every loop hands you a tidy variable that obviously shrinks. The measure can be any expression you build from the program's state, as long as it lands in a well-founded set. For a loop that walks an index i upward from 0 to n, the natural measure is the gap n - i: it starts at n, drops by at least 1 each pass, and bottoms out at 0. For a recursive routine, the measure is whatever shrinks on each call — the size of the subarray, the depth still to go — which is exactly the foundation under induction on recursive calls.
Sometimes a single number is not enough and you need a tuple compared in dictionary order: first by the most significant component, ties broken by the next, and so on. A nested loop where the inner counter resets is a classic case — the inner count alone goes up and down, but the pair (work-left-outer, work-left-inner) strictly decreases in lexicographic order every step. Lexicographic order on tuples of non-negative integers is itself well-founded, so the same staircase argument applies, just on a richer staircase.
One honest caveat the technique does not hide: a measure proves termination, never speed. Knowing b strictly drops tells you Euclid stops; it does not, by itself, tell you it stops fast. And a measure that decreases by only 1 each time out of a starting value of 2^n proves termination yet describes an exponential-time loop. Termination and efficiency are different questions, answered by different arguments — keep them in separate drawers.
Putting both halves together
Total correctness is now a two-column checklist, and a full proof simply fills both columns. The invariant column (from the previous guides) shows the answer is right if we stop; the measure column (this guide) shows we do stop. Crucially, these two arguments live side by side without interfering: the invariant talks about what is true each round, the measure talks about how much closer to done each round is. You design and verify them independently, then staple them together.
It is worth resisting the temptation to skip the measure because termination 'feels obvious.' The most embarrassing bugs are infinite loops on an edge case: a search that fails to move its pointer when two keys are equal, a recursion whose subproblem is not actually smaller, a `while x != 0` that should have been `while x > 0` for a value that overshoots past zero. Each is a measure that fails to strictly decrease on exactly one input. Writing the measure down is how you catch these before your users do — proof over plausibility, every time.
In the final guide of this rung we cash in everything: a complete, two-column proof of insertion sort and of binary search, invariant and measure together, start to finish. With the decreasing measure now in your toolbox, you have the second half of every total-correctness argument you will ever write.