1.9 循环不变量

上一篇教你怎么分析算法快不快（复杂度），这一篇教你怎么证明算法对不对（正确性）。前者是渐近分析，后者的核心武器就是循环不变量（loop invariant）。它在 1.1 插入排序和 1.3 二分查找里都埋过伏笔，这一篇我们把这套证明语言正式讲透，并拿那两个算法当范例收口。

1.为什么需要循环不变量

写完一个带循环的算法，你怎么相信它真的得到了正确答案？"我跑了几组测试都对了"不算证明——测试只能覆盖有限输入，证明要对所有输入成立。循环不变量就是给迭代算法做这种证明的标准框架。

它的精神，和数学归纳法一脉相承：找到循环每一步都保持不变的那个性质，证明它在循环开始、循环中、循环结束时都成立，最后由"循环结束时的不变量"推出"结果正确"。

2.循环不变量的三步法

对一个循环，要证明三件事：

第一步·初始化（Initialization）。 循环开始前（第一次迭代之前），不变量成立。这相当于归纳法的基底。

第二步·保持（Maintenance）。 假设某次迭代开始时不变量成立，证明这次迭代执行完后，不变量仍然成立。这相当于归纳法的归纳步。

第三步·终止（Termination）。 循环结束时，结合"不变量成立"和"循环为什么停"，推出算法得到了正确结果。这一步是归纳法没有的——循环会停，停的那一刻我们要榨出有用的结论。

注意第二步和第三步的区别：第二步只管"不变量维持住了"，不负责结论；结论由第三步在循环结束时给出。很多人把这两步混在一起，证明就乱了。

3.范例一：插入排序的正确性

回到 1.1 的插入排序。它的循环不变量是：

不变量：在每轮外层循环（指标 $j$）开始时，子数组 $A[1..j-1]$ 是原来 $A[1..j-1]$ 那些元素的有序排列。

（"原来那些元素的有序排列"——强调元素集合不变、只是排了序。）三步走：

初始化。 $j=2$ 时，$A[1..1]$ 只有一个元素，一个元素的数组天然有序，且就是原来的那个元素。不变量成立。✓

保持。 假设某轮 $j$ 开始时 $A[1..j-1]$ 有序。内层 while 把 $A[j-1], A[j-2], \dots$ 里所有 $>key$ 的往右挪一格，停在第一个 $\le key$ 的位置，然后把 $key$ 放进空位。结果是 $A[1..j]$ 也变有序了。下一轮 $j\leftarrow j+1$ 开始时，不变量（$A[1..(j+1)-1]=A[1..j]$ 有序）正好成立。✓

终止。 循环在 $j=n+1$ 时结束。代入不变量：$A[1..n]$ 是原来 $n$ 个元素的有序排列——正是排序的目标。✓

三步齐了，插入排序的正确性证毕。你看，整个证明的核心就是那句不变量，剩下都是机械的三步验证。

4.范例二：二分查找的正确性

再看 1.3 的二分查找。它的循环不变量是：

不变量：如果目标在数组中，它一定在闭区间 $[lo, hi]$ 内。

三步走：

初始化。 第一次循环前 $lo=1, hi=n$，区间是整个数组，目标若存在当然在里面。✓

保持。 假设某轮开始目标若存在则必在 $[lo,hi]$。看 $mid=\lfloor(lo+hi)/2\rfloor$：

• 若 $A[mid]=target$，直接返回找到，循环终止，无需保持。
• 若 $A[mid]<target$，则目标（若存在）只可能在 $mid$ 右侧，令 $lo=mid+1$，新区间 $[mid+1,hi]$ 仍包含目标（若存在）。
• 若 $A[mid]>target$，类似地令 $hi=mid-1$，目标（若存在）仍在 $[lo,mid-1]$。

每种情况都维持了"目标若存在则在新区间内"。✓

终止。 循环在 $lo>hi$ 时结束（区间空了）。结合不变量：若目标存在，它应在 $[lo,hi]$ 内，但区间已空，矛盾——所以目标不存在，返回 -1 正确。✓

这就是为什么二分查找是对的——它从头到尾死守"$[lo,hi]$ 一定含目标（若存在）"这条不变量，每一步 +1/-1 都是为了在排除 $mid$ 后仍维持它。理解了这条不变量，二分查找的所有边界细节都不再是"死记"，而是"必然"。

5.不变量是一种设计工具，不只是证明工具

到这里你可能觉得不变量只是"事后证明用"的。其实更强：它是事前设计用的。 好的算法往往是先想清楚"我要维持什么不变量"，再倒推出代码该怎么写。

拿二分查找的 lower_bound（1.3 提过的"找第一个 $\ge target$ 的位置"）举例。它的不变量是"$[lo,hi)$ 这个半开区间是答案的候选"，于是代码自然长成 while lo < hi、hi = mid（不 -1，因为 $mid$ 可能就是答案，要留在区间里）、最后 return lo。先定不变量，代码就是不变量的忠实翻译，不用死背带不带等号。

这种"先想不变量再写代码"的思维，到了第十一卷（算法设计的统一视角）会变成一个正式的设计方法——不变量法（11.1）。现在你先体会：不变量不只是用来证对的，更是用来想对的。

6.不变量和数学归纳法的关系

你可能已经感觉到循环不变量和数学归纳法很像。确实：

• 初始化 ↔ 归纳基底
• 保持 ↔ 归纳步
• 终止 ↔ （归纳法没有，因为归纳是无穷的，循环是有限的）

唯一的区别在第三步：数学归纳法证明"对所有自然数成立"，没有终点；循环不变量证明的是"循环结束时结论成立"，有终点，所以要多一步"在终止时榨出结论"。这一步往往是整个证明最出结论的地方——循环结束的那个条件，恰恰是把不变量转化成最终结果的钥匙。

7.练习

Q1. 用循环不变量证明：下面这个求最大元素的简单循环是正确的。

m = A[1]
for i = 2 to n:
    if A[i] > m: m = A[i]

不变量：每轮 $i$ 开始时，$m$ 是 $A[1..i-1]$ 中的最大值。 初始化：$i=2$，$m=A[1]$ 是 $A[1..1]$ 的最大值。✓ 保持：若 $A[i]>m$ 则 $m\leftarrow A[i]$，新 $m$ 是 $A[1..i]$ 最大；否则 $m$ 已 $\ge A[i]$，仍是 $A[1..i]$ 最大。下一轮 $i+1$ 开始时不变量（$m$ 是 $A[1..i]$ 最大）成立。✓ 终止：$i=n+1$，$m$ 是 $A[1..n]$ 最大值。✓

Q2. 二分查找的循环不变量为什么是"目标若存在则在 $[lo,hi]$ 内"，而不是"目标在 $mid$"？后者会出什么问题？

因为 $mid$ 每轮都变，"目标在某个具体的 $mid$"既不稳定也没用——不变量必须是整个循环期间恒成立的性质，且和最终结论挂钩。"$[lo,hi]$ 含目标"这个性质，每轮调整边界后仍然成立，且循环结束时（区间空）能直接推出"目标不存在"。换成"目标在 $mid$"，下一轮 $mid$ 变了它就破了，没法维持，证明无从下手。

Q3.（思考题） 为什么说循环不变量"不只是证明工具，更是设计工具"？用自己的话解释。

因为好的算法往往是先确定"要维持什么不变"，代码是把这个不变量翻译成操作。比如二分的各种变体（找等于、找下界、找上界），它们代码不同正是因为维持的不变量不同——先想清楚区间是闭还是半开、$mid$ 留不留，边界写法就唯一确定了。这种"不变量先行"的思维让人不必死背边界，而是从不变量推导出代码。第十一卷 11.1 会把这一点提炼成正式的设计方法。

8.小结

循环不变量是证明迭代算法正确性的标准武器，三步法（初始化、保持、终止）对应数学归纳法的基底和归纳步，外加一个"终止时榨结论"。但它不止于证明——它更是一种设计思维：先想清楚要维持什么不变，再让代码忠实表达它。卷一到此，你已经学会了实现算法（1.1–1.7）和分析算法（1.8 复杂度、1.9 正确性）这两门基础语言。第二卷我们带着这套语言，去看分治思想怎么把排序、选择、几何、矩阵、多项式乘法这些看似无关的问题统一到同一套结构之下。