基礎與複雜度
迴圈不變量
迴圈不變量是這樣一句話：每當迴圈轉回來時它都為真——第一趟之前為真，每一趟之後為真，迴圈最終停下時也為真。在所有變來變去的變數當中，它是你可以倚靠的那個穩定事實。一個樸素的類比：當你一級一級往上爬樓梯時，不變量是「我下方的每一級台階都已經被爬過了」。你腳下的那一級在不停變化，但這句話在最底下為真、每爬一級之後為真、爬到頂上也為真——而到了頂上，它告訴你一件有用的事：整段樓梯都爬完了。
程式設計師用不變量來論證一個迴圈為什麼正確，而不只是看它碰巧在幾個測試案例上給出了對的答案。這個論證分三部分，很像數學歸納法。初始化：迴圈開始之前不變量為真。保持：若它在某一趟迭代開始時為真，迴圈體會讓它在這一趟結束時仍為真。終止：當迴圈退出時，不變量——結合「迴圈為何停下」這個理由——給出你想要的結果。找到那個對的不變量，往往就是一個棘手的迴圈忽然說得通的那一刻。
拿一個從左到右掃描、求陣列最大值的迴圈來說。一個好的不變量是：「max 持有目前為止見過的元素（a[0..i-1]）中的最大值。」在我們看任何東西之前它就為真（空集意義下成立，把 max 設為第一個元素），每一步透過與新元素比較來保持它，而當掃描結束——已見過每一個元素——不變量便說 max 是它們全體中最大的。不變量把「我覺得這能行」變成了「我看得出它為什麼能行」，這正是它配得上一個名字的全部理由。
int mx = a[0]; // invariant holds for a[0..0]
for (int i = 1; i < n; ++i) { // maintain: extend to a[0..i]
if (a[i] > mx) mx = a[i];
} // termination: mx = max of a[0..n-1]「max 是目前為止見過的最大值」這一不變量，開始時為真、每趟保持、結束時證明了正確性。
證明分三部分：初始化、保持、終止——它是數學歸納法在迴圈上的對應物。
又稱
另見