1. 什么是循环不变式？
循环不变式（Loop Invariant）是用于证明算法正确性的重要工具。它是一个在循环执行过程中始终保持为真的条件（或逻辑表达式），帮助我们推理算法在每次迭代中对数据的处理是否符合预期。
使用循环不变式可以增强我们对算法行为的理解，尤其是在设计和验证复杂算法时非常有用。
2. 循环不变式的作用
循环不变式主要用于以下目的：
✅ 验证算法是否在每一步都维护了正确的中间状态
✅ 证明算法最终输出的结果是正确的
✅ 在调试时帮助定位逻辑错误（即不变式被破坏的地方）
它的核心思想类似于数学归纳法：
- 初始成立：在循环第一次迭代前成立
- 保持成立：如果在某次迭代前成立，那么在下一次迭代前也必须成立
如果这两点都能证明，那么我们可以确定该不变式在整个循环过程中始终成立。
3. 如何构造和证明循环不变式？
3.1 构造一个合适的不变式
一个好的循环不变式应满足以下条件：
- 简洁：表达清晰，易于理解和验证
- 相关：与算法目标直接相关
- 可维护：在每次迭代中能够被维护
- 终止后有用：循环结束时不变式能说明算法正确性
举个例子：我们想编写一个函数来计算数组所有元素的和：
int sumArray(int[] a) {
int s = 0;
for (int i = 0; i < a.length; i++) {
s += a[i];
}
return s;
}
我们可以构造一个不变式：
在第 i 次迭代开始时，变量 s 的值等于 a[0] 到 a[i-1] 的和。
这个不变式在循环结束时（i == a.length）就表示 s 是整个数组的总和，从而验证了算法的正确性。
3.2 证明不变式成立
证明一个循环不变式通常分为两个步骤：
初始成立（Initialization）
确保在第一次迭代前不变式为真保持成立（Maintenance）
假设在某次迭代前不变式为真，证明下一次迭代前它仍然为真
这两个步骤共同保证了不变式在整个循环过程中始终为真。
⚠️ 注意：循环不变式并不需要在循环体内每一步都为真，只要在每次迭代开始前成立即可。
4. 示例一：二进制加法
我们来看一个更复杂的例子：两个 n 位二进制数相加。
int[] addBinary(int[] x, int[] y) {
int n = x.length;
int[] z = new int[n + 1];
int c = 0;
for (int i = 0; i < n; i++) {
z[i] = (x[i] + y[i] + c) % 2;
c = (x[i] + y[i] + c) / 2;
}
z[n] = c;
return z;
}
4.1 构造不变式
在第 i 次迭代开始时，z[0..i-1] 和进位 c 组成的二进制数等于 x[0..i-1] 和 y[0..i-1] 的和。
4.2 证明不变式成立
- 初始成立：i = 0 时，z[0..-1] 表示空数组，c = 0，和为 0，成立
- 保持成立：假设在第 i 次迭代前成立，那么在第 i 次迭代中我们计算了 z[i] 和新的 c，它们的组合仍然等于 x[0..i] 和 y[0..i] 的和
最终在循环结束后，z[0..n] 就是 x 和 y 的完整和。
5. 示例二：插入排序（Insertion Sort）
void insertionSort(int[] a) {
for (int j = 1; j < a.length; j++) {
int key = a[j];
int i = j - 1;
while (i >= 0 && a[i] > key) {
a[i + 1] = a[i];
i--;
}
a[i + 1] = key;
}
}
5.1 构造不变式
在 for 循环的每次迭代开始时，a[0..j-1] 是已排序的子数组，包含原始 a[0..j-1] 中的所有元素。
5.2 证明不变式成立
- 初始成立：j = 1 时，a[0] 是一个单元素数组，自然有序
- 保持成立：在第 j 次迭代中，将 a[j] 插入到 a[0..j-1] 的合适位置，使得 a[0..j] 仍保持有序
循环结束后，j == a.length，整个数组 a 就是有序的。
6. 常见“平凡成立”情况
在证明初始成立时，我们常常会用到一些“平凡成立”（trivially true）的语句，比如：
- 一个元素的数组是有序的 ✅
- 一个空数组的和为 0 ✅
- 一个空集合不包含任何元素 ✅
这些语句不需要进一步证明，可以直接作为初始条件使用。
7. 总结
循环不变式是验证算法正确性的有力工具，尤其适用于迭代算法。使用它时要注意：
- 不变式必须在每次迭代开始前成立
- 它应该能反映算法当前状态与目标状态之间的关系
- 不变式在循环结束后应能说明算法的最终正确性
通过构造和证明不变式，不仅可以增强我们对算法的理解，还能帮助我们在开发过程中尽早发现潜在的逻辑错误。