基础与复杂度
循环不变量
循环不变量是这样一句话：每当循环转回来时它都为真——第一趟之前为真，每一趟之后为真，循环最终停下时也为真。在所有变来变去的变量当中，它是你可以倚靠的那个稳定事实。一个朴素的类比：当你一级一级往上爬楼梯时，不变量是「我下方的每一级台阶都已经被爬过了」。你脚下的那一级在不停变化，但这句话在最底下为真、每爬一级之后为真、爬到顶上也为真——而到了顶上，它告诉你一件有用的事：整段楼梯都爬完了。
程序员用不变量来论证一个循环为什么正确，而不只是看它碰巧在几个测试用例上给出了对的答案。这个论证分三部分，很像数学归纳法。初始化：循环开始之前不变量为真。保持：若它在某一趟迭代开始时为真，循环体会让它在这一趟结束时仍为真。终止：当循环退出时，不变量——结合「循环为何停下」这个理由——给出你想要的结果。找到那个对的不变量，往往就是一个棘手的循环忽然说得通的那一刻。
拿一个从左到右扫描、求数组最大值的循环来说。一个好的不变量是：「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 是目前为止见过的最大值」这一不变量，开始时为真、每趟保持、结束时证明了正确性。
证明分三部分：初始化、保持、终止——它是数学归纳法在循环上的对应物。
又称
另见