a well-founded termination measure

An invariant proof tells you a loop or recursion gives the right answer IF it stops, but not that it stops. To prove it stops, you attach a number to the current state — a measure — that strictly decreases every iteration (or every recursive call) and cannot decrease forever. Like a countdown timer or a staircase you only ever walk down: if every step takes you to a strictly lower stair and there is a bottom stair, you must reach the bottom in finitely many steps. That guarantees termination.

Two conditions make a measure work. First, it must strictly decrease at every step. Second, the values it takes must be well-founded: there is no infinite strictly-decreasing chain. The non-negative integers are the standard choice — you cannot subtract 1 from a non-negative integer forever without hitting 0 and being unable to go lower. So you find a quantity, show it is a non-negative integer (or some well-founded value), and show each iteration makes it strictly smaller. For binary search the measure is the window size hi - lo + 1, which strictly shrinks every step until it cannot stay positive. For Euclid's GCD, gcd(a,b) -> gcd(b, a mod b), the second argument strictly decreases and stays >= 0, so the recursion must bottom out. For a 'while x > 0: x = x - 3' loop, x itself (rounded as needed) is the measure.

Why 'well-founded' and not just 'decreasing'? A measure that decreases but lives in, say, the positive reals could shrink forever (1, 1/2, 1/4, ...) without ever stopping — that is the trap. Well-foundedness rules out infinite descent. This is exactly the termination half of total correctness; the measure is sometimes called a variant (it changes, in contrast to the invariant that stays the same). The honest difficulty: finding the right measure can be subtle for loops whose progress is not the obvious counter, and for some programs no simple integer measure exists.