良基終止度量（well-founded termination measure）

不變量證明告訴你「若迴圈或遞迴停下來，它會給出正確答案」，卻沒說它會停。要證明它會停，你給當前狀態貼上一個數——一個度量——讓它在每一輪（或每次遞迴呼叫）都嚴格遞減，且不可能永遠遞減。就像倒數計時器，或一座你只往下走的樓梯：若每一步都把你帶到嚴格更低的階，而且有最底一階，那你必定在有限步內到底。這就保證了停機。

讓一個度量奏效需要兩個條件。第一，它必須在每一步嚴格遞減。第二，它所取的值必須是良基的：不存在無窮嚴格遞減鏈。非負整數是標準選擇——你不可能對一個非負整數一直減 1 而不碰到 0、再也無法更低。所以你找一個量，證明它是非負整數（或某種良基的值），再證明每一輪都讓它嚴格變小。二分搜尋的度量是窗口大小 hi - lo + 1，它每步嚴格縮小，直到無法維持為正。歐幾里得的 GCD，gcd(a,b) -> gcd(b, a mod b)，第二個引數嚴格遞減且保持 >= 0，所以遞迴必定見底。對於「while x > 0: x = x - 3」的迴圈，x 本身（必要時取整）就是度量。

為何要「良基」而不只是「遞減」？一個會遞減但住在例如正實數中的度量，可能永遠縮小（1, 1/2, 1/4, …）卻永遠停不下來——這正是陷阱。良基性排除了無窮下降。這恰好是完全正確性的「終止」那一半；這個度量有時被稱為變式（variant，它會變，對比於保持不變的 invariant）。誠實的難處：對於進展不是顯而易見計數器的迴圈，找對度量可能很微妙；而對某些程式，根本不存在簡單的整數度量。