迴圈不變量（loop invariant）

想像你端著托盤爬梯子。你心裡要一直默念的，不是「我現在在第幾階」，而是「托盤還是平的」。如果你出發時托盤是平的，而且每跨一步都讓它保持平，那麼當你爬到頂端時它仍然是平的——不管中間有幾階。迴圈不變量正是這種陳述：一個關於程式變數的性質，在迴圈的每一輪都保持為真，於是當迴圈結束時，你就能從它讀出究竟完成了什麼。

嚴格來說，迴圈不變量是我們附加在迴圈上、並分三部分證明的主張。初始化：在第一輪之前它為真。維持：若它在某一輪之前為真，則在下一輪之前仍為真（迴圈本體保住它）。終止：當迴圈離開時，不變量連同離開條件一起告訴我們迴圈完成了任務。這個樣式正對應歸納法：初始化是基底情形，維持是歸納步驟，終止則兌現結論。例如在插入排序中，不變量是「前綴 A[1..i-1] 已排序，且含有原本最前面的 i-1 個元素」；它在迴圈前成立，每一步把 A[i] 插入仍保持為真，最後整個陣列就排好序了。

選一個好的不變量才是真正的技藝：太弱，結束時它什麼有用的事都告訴不了你；太強，你又證不出「維持」。不變量要夠強，強到與離開條件結合後能推出你要的結論，但又恰好是每一輪都能保住的那種東西。一旦找到對的不變量，正確性證明幾乎就自動寫好了——所以思考的重點在於找出不變量，而不是證明的瑣碎記帳。