不變量給不了你的那一半正確性
在前三篇裡，你學會了論證答案是對的：一個迴圈不變量在每一次迭代中都成立，而「當迴圈停下來時」，不變量加上離開條件就釘住了正確的輸出。請再讀一次這句話，因為它藏著一個大如穀倉的漏洞：「當迴圈停下來時」。不變量對於迴圈究竟會不會停下來，什麼都沒承諾。一個永遠空轉的迴圈永遠到不了它的終止步驟，所以它永遠不會給出錯誤答案——但它也永遠不會給出任何答案。
這正好就是你先前遇過的兩種正確性之間的鴻溝。部分正確性說：「如果」程式停了，答案就是對的。完全正確性說：程式會停下來「而且」答案是對的。不變量替你買到的是部分正確性。要升級到完全正確性，你必須另外、明確地證明終止。好消息是：整件事基本上只有一個工具，而且它優美地簡單。
遞減的度量，以及它為何有效
整個想法用一句話講完。要證明一個迴圈會終止，給它附上一個量——稱作度量或變式——並證明兩件事：每一次迭代都讓這個度量「嚴格變小」，而且這個度量「不可能跌破某個底線」。一個嚴格遞減、卻又永遠不能低於零（而且只以整數步前進）的值，不可能永遠一直減下去；它必定在有限步內觸底，於是迴圈被迫停下來。
經典的度量是一個非負整數。把它想成你腳下還剩的階梯數：每一步至少嚴格往下一階，而且有一層地面。你或許不知道究竟還剩幾步，但你知道那是有限的，因為你不可能在一座有限的樓梯上永遠往下走。這幅圖像——朝著一條不可打破的底線嚴格下降——就是整個引擎。我們把任何這樣的量稱作良基度量，「良基」正是用來描述一個沒有無窮下降鏈的排序的精確詞語。
一個微型證明範例：歐幾里得的最大公因數
讓我們來證明我們手上最古老的非平凡演算法——歐幾里得求最大公因數的方法——會終止。它的部分正確性建立在 gcd(a, b) = gcd(b, a mod b) 這個事實上；這一塊屬於gcd 正確性證明，這裡我們直接當作已知。我們現在想要的是「另外」那一半：這個迴圈總是會結束。
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- 選定度量。令度量就是 b 本身，也就是第二個變數。由於迴圈只在 b 不為 0 時運行，而 b 是一個餘數，b 永遠是非負整數——所以它有一條位於 0 的底線。
- 證明它嚴格遞減。一次迭代把 (a, b) 換成 (b, a mod b)。b 的新值是 a mod b，也就是 a 除以 b 的餘數。根據餘數的定義，0 <= a mod b < b。所以新的 b 嚴格小於舊的 b。嚴格下降：確認。
- 套用原理。我們有一個每次迭代都嚴格遞減的非負整數。它在抵達 0 之前，下降的次數不可能超過（b 的起始值）那麼多。當 b 抵達 0，while 條件不成立，迴圈離開。因此 GCD 在每一筆合法輸入上都會終止。
注意這有多省力。我們完全不需要知道「跑幾次」迭代——那是另一個更難的問題，其答案恰好是 O(較小那個輸入的對數)。終止只需要運動的「方向」加上一條底線，從不需要精確的距離。這正是這項技巧反覆帶來的輕鬆感：證明一個迴圈會結束，幾乎總是遠比計算它要花多久來得容易。
超越單一整數的度量
並不是每個迴圈都會遞給你一個明顯會縮小的乾淨變數。度量可以是你用程式狀態建構出來的任何運算式，只要它落在一個良基的集合裡就行。對於一個讓索引 i 從 0 往上走到 n 的迴圈，自然的度量是「差距」n - i：它從 n 開始，每一輪至少降 1，並停在 0。對於一個遞迴的副程式，度量就是每次呼叫時會縮小的那個東西——子陣列的大小、還要往下的深度——這正好就是對遞迴呼叫做歸納底下的基礎。
有時單一個數字還不夠，你需要一個用「字典序」比較的「元組」：先比最重要的分量，相同時再比下一個，依此類推。一個內層計數器會重設的巢狀迴圈就是經典案例——光看內層計數會上上下下，但配對 (外層剩餘工作量, 內層剩餘工作量) 在每一步都依字典序嚴格遞減。非負整數元組上的字典序本身就是良基的，所以同樣的樓梯論證照樣適用，只是換成了一座更豐富的樓梯。
這項技巧不會藏起的一個誠實的但書：度量證明的是終止，從來不是「速度」。知道 b 嚴格下降告訴你歐幾里得會停；它本身並沒有告訴你它停得很快。而一個從 2^n 的起始值每次只降 1 的度量，證明了終止，卻描述的是一個指數時間的迴圈。終止與效率是不同的問題，由不同的論證來回答——把它們放在不同的抽屜裡。
把兩半合在一起
完全正確性現在是一份兩欄的檢查表，而一個完整的證明就只是把兩欄都填滿。不變量這一欄（來自前幾篇）證明：「如果」我們停下來，答案就是對的；度量這一欄（本篇）證明：我們「確實」會停下來。關鍵在於，這兩個論證並排存在卻互不干擾：不變量談的是每一輪「什麼」為真，度量談的是每一輪「離完成更近多少」。你獨立地設計並驗證它們，然後再把它們釘在一起。
值得抵抗那種因為終止「感覺很明顯」就跳過度量的誘惑。最難堪的臭蟲就是在某個邊界案例上的無窮迴圈：一個在兩個鍵相等時忘了移動指標的搜尋、一個子問題其實沒有變小的遞迴、一個對某個會衝過零的值本該寫成 `while x > 0` 卻寫成 `while x != 0` 的迴圈。每一個都是某個度量在恰好某一筆輸入上沒能嚴格遞減。把度量寫下來，正是你搶在使用者之前抓到這些問題的方法——永遠以證明取代看似合理。
在本階段的最後一篇，我們會把一切兌現：對插入排序與二分搜尋做一個完整的、兩欄式的證明，不變量與度量並陳，從頭到尾。有了遞減度量進到你的工具箱，你已經握有將來會寫的每一個完全正確性論證的後半部。