循环不变式

概述

循环不变式 是在循环的每次迭代前后都保持为真的断言，类似于数学归纳法，用于证明算法的正确性。它是CLRS中证明迭代算法正确性的核心工具。

定义

循环不变式

循环不变式是一个关于循环变量和数组元素的断言 $P$，满足以下三条性质：

1. 初始化（Initialization）：循环第一次迭代之前，$P$ 为真。
2. 保持（Maintenance）：如果在某次迭代之前 $P$ 为真，那么在本次迭代之后 $P$ 仍然为真。
3. 终止（Termination）：循环终止时，$P$ 为真，且结合终止条件可推出算法的正确性。

核心性质

• 循环不变式与数学归纳法高度对应：初始化对应归纳基础，保持对应归纳步骤。
• 循环不变式不一定在循环体执行过程中保持为真，只在每次迭代的开始和结束时刻为真。
• 选择恰当的循环不变式是证明的关键，通常需要反映算法的”设计意图”。

章节扩展

第2章：入门

• 2.1 插入排序：以插入排序为例，循环不变式为”子数组 $A[\mathrm{1..}j-1]$ 由原来在 $A[\mathrm{1..}j-1]$ 中的元素组成，且已排好序”。
• 2.3 分治法：归并排序的正确性通过递归（而非循环不变式）来证明，但循环不变式用于证明 MERGE 过程的正确性。

参见

• 插入排序
• 归并排序
• 伪代码