形式陈述

断言 $I$ 是循环不变式，若满足：初始化时 $I$ 成立；假设某轮开始 $I$ 成立，执行循环体后下一轮开始仍成立；循环结束时 $I$ 与退出条件共同蕴含后置条件。

直觉

不变式描述循环每走一步都不会丢失的“已完成工作”。它把无限多种迭代次数压缩成一次归纳论证。

例子与边界

插入排序第 $j$ 轮开始时，前缀 $A[0..j)$ 已排序且包含原前缀的同一批元素。仅证明不变式保持不能证明循环终止，还需变式量或其他终止论证。

推论与应用

循环不变式用于排序、图遍历、动态规划和数据结构操作的正确性证明。

参考资料

• Thomas H. Cormen et al., Introduction to Algorithms, 4th ed., §2.1.
• C. A. R. Hoare, “An Axiomatic Basis for Computer Programming,” 1969.