梯子上的托盤：一件從不傾倒的真實之事
上一篇指南留給我們一個當時還無法滿足的要求：一個迴圈會跑幾次取決於輸入，那我們要怎麼一次論證它在「每一個」輸入上產生什麼？追蹤一個例子只會告訴你那個例子的事——而我們已經講好測試不是證明。答案是：別再去追那個不斷變化的狀態，改為替「貫穿這場翻騰仍保持為真的某件事」取個名字。那件事就是迴圈不變量。
想像你端著一盤茶爬梯子。值得一直默念的不是「我現在在第幾階」——那每一步都在變，幾乎沒給你什麼訊息。值得默念的是「托盤還是平的」。如果你踏出第一步前托盤是平的，而且每一步都讓它保持平，那麼爬到頂端時它仍然是平的，不管中間有幾階。迴圈不變量正是那句「托盤是平的」陳述：一個關於程式變數的性質，在迴圈邊界的每一輪都為真，而且刻意挑成這樣——當爬升結束時，它能告訴你你完成了什麼。
更深一層的點子是：不變量把一個沒有上界的問題（「跑遍所有輪次會發生什麼？」）轉成一個有界的問題（「一輪對這一句陳述做了什麼？」）。你從不一次推理整段執行；你只推理單獨一步，再由一條結構性原理把這些單獨的步驟縫成對整個迴圈的保證。那條原理就是歸納法，而本指南接下來要做的，就是把它講得乾淨到足以信任。
三項義務：初始化、維持、終止
要使用一個不變量，你必須恰好履行三項義務。初始化：在迴圈第一次執行之前，不變量為真。維持：若不變量在某一輪開頭為真，迴圈本體會讓它在下一輪開頭仍為真。終止：當迴圈最終離開時，不變量——連同它離開的原因——會給你想要的結果。三項都做到，迴圈就被證明正確（前提是它會停，這點稍後會回來談）。
注意維持那句話的措辭很講究：你只假設「當前這一輪」的不變量，再對「下一輪」重新證明它。你絕對不准假設最終答案，也不准假設某個更後面輪次的不變量——那等於把你要證明的東西先當作前提。你假設某一階托盤是平的，再證明你跨那單獨一步能讓下一階托盤仍然平。正是這種局部、一步性的特質，讓這項義務變得可檢驗：你只需盯著迴圈本體與資料，永遠不必盯著那整段沒有上界的執行。
它為何奏效：迴圈不變量是披著外衣的歸納法
這三項義務不是一份隨意的清單；它們就是穿著程式設計師衣服的數學歸納法。令 P(k) 為「不變量在第 k 輪開頭成立」這句陳述。初始化是基底情形 P(0)：第一輪之前為真。維持是歸納步驟：P(k) 推出 P(k+1)，因為本體把不變量從一個邊界帶到下一個邊界。由歸納法，P(k) 對每個 k 都成立——不變量在每一輪開頭都為真，不論最後究竟有幾輪。這正是「托盤一路保持平」之所以有保證的全部理由。
看出這個等價，在兩個方向上都有回報。它告訴你「為何輕忽基底情形要付出代價」：有歸納步驟卻沒有成立的基底，什麼都證明不了，正如有維持論證卻有錯誤的初始化也什麼都證明不了——骨牌根本沒開始倒。它也告訴你終止這項義務做了歸納法本身辦不到的事：它藉由再加上一個事實（否定後的迴圈條件），把「每一輪的承諾」兌現成關於「最終」狀態的陳述。歸納讓托盤保持平；離開條件則告訴你你把它放到了哪一層架上。
一個走過全程的微型證明：陣列求和
讓我們在最小卻誠實的例子上把整套機器跑一遍。我們要對含 n 個數的陣列 A 求和。迴圈維持一個累加值 s 與一個下一個索引 i。在陳述任何義務之前，我們先承諾一個不變量，而技藝就在於把它選好：不是「s 是某個部分和」（太含糊），而是把 s 精確繫到「究竟哪些元素已被加進去」的那個主張。
s = 0
i = 1
while i <= n: # invariant: s == sum of A[1..i-1]
s = s + A[i]
i = i + 1
return s- 初始化。第一輪之前，i = 1、s = 0。不變量主張 s 等於 A[1..0] 之和，而這是個空範圍，其和為 0。所以 s = 0 對得上，不變量成立——是在「沒看任何元素」的情況下建立的，這恰恰正確。
- 維持。假設某一輪開頭 s == A[1..i-1] 之和。本體執行 s = s + A[i]，於是現在 s == A[1..i] 之和；接著 i = i + 1，故就新的 i 而言這讀作 s == A[1..(新 i)-1] 之和。不變量在下一個邊界重新建立，而且只用到了這一輪的歸納假設。
- 終止。迴圈在 i <= n 時繼續，所以它恰好在 i = n + 1 時離開。把這個確切的離開值代入不變量，得 s == A[1..n] 之和——整個陣列的和，正是我們一開始要算的。把邊界讀成 n+1（而非 n），是那個能抓出差一錯誤的誠實動作。
不變量證明了什麼——又遺漏了什麼
再讀一次求和證明的終止那一行，注意一個被藏起來的假設：「迴圈在 i = n+1 時離開」。我們「假設」了它會離開。三項不變量義務全部加起來，只證明了一個條件式：「若」迴圈停下來，結果就正確。它們對「迴圈到底會不會停」隻字未提。這個較弱的保證有個名字——叫做部分正確性。一個永遠跑下去的迴圈，荒謬地說是部分正確的，因為它從不給出錯誤答案（它根本不給答案）。
要升級成完全正確性——迴圈會停「而且」答案正確——你需要第二個、獨立的論證，證明迴圈一定會停。標準工具是一個遞減度量：貼在狀態上的一個非負整數，每一輪都嚴格下降。在求和迴圈裡，這個度量是 n - i + 1，也就是還剩幾輪要跑；它從 n 開始，每一輪減一，而一個非負整數不可能永遠下降，所以迴圈一定會抵達離開點。本階段的第 4 篇指南專門用來建構這些度量；現在只要把這個區分牢牢記住。
所以完整的圖像是一個乾淨的加總：完全正確性 = 部分正確性（一個不變量，由歸納法證明）+ 終止（一個遞減度量）。同一套模板從這個玩具例子一路放大到那些經典。在插入排序中，不變量是「前綴 A[1..i-1] 已排序且含有原本最前面的 i-1 個元素」，而迴圈索引提供了度量；在二分搜尋中，不變量把目標釘在一個不斷縮小的窗口裡，而那個窗口的寬度就是度量。在求和迴圈上把這三件套練熟，你就握有了在爬這條階梯途中會遇到的每一個迴圈證明的骨架。