算法正确性证明之循环不变量

1. 循环不变量基本概念

• 循环不变量定义：
  在循环执行过程中，在每一次迭代（通常在循环体开始或结束处）所满足的某个条件称为循环不变量。

• 证明目标：
  证明循环不变量在循环的每一步都成立，从而推导出循环结束时算法所需要达到的正确状态或目标。

---

2. 循环不变量证明的三个基本步骤

循环不变量证明通常包含三个部分：

2.1 初始化（Initialization）

证明在第一次进入循环体时，循环不变量成立。

• 理论推导：
  检查循环开始前（或第一轮迭代开始时）的变量状态，验证不变量条件是否成立。

• 关键作用：
  确保递归证明的基础正确性，为后续维护和归纳提供起点。

2.2 保持（Maintenance）

证明如果在某次迭代开始时循环不变量成立，那么在完成该次迭代后，不变量依然成立。

• 理论推导：
  假设在第 k 次迭代前，不变量成立，证明经过第 k 次迭代后，不变量依然成立，即满足第 k+1 次迭代开始时的状态。

• 关键作用：
  通过归纳假设，保证在每一次循环更新中，不变量得以维持，从而整个循环过程中不变量一直成立。

2.3 终止（Termination）

证明当循环结束时，不变量提供了足够的信息，证明了算法达到预期目标。

• 理论推导：
  分析循环退出条件下的变量状态，根据不变量得出循环结束时的结果满足问题的正确性要求。

• 关键作用：
  将循环不变量的保持和初始化条件综合，说明最终状态必然满足算法设计目标，完成正确性证明。

---

3. 理论推导过程示例

以一个简单算法为例：插入排序。证明其在每次循环迭代后“已排序部分”保持有序的不变量。

1. 初始化：

   • 当数组只有一个元素时，显然是有序的。

   • 初始时，不变量“数组的前 iii 个元素是有序的”成立（当 i=1 ）。

2. 保持：

   • 假设在第 i 次迭代时，前 i 个元素已经有序。

   • 在第 i+1 次迭代中，将第 i+1 个元素插入到前 iii 个元素中合适的位置。

   • 插入后，前 i+1 个元素仍然保持有序。

   • 因此，循环不变量得以保持。

3. 终止：

   • 当 i=n（数组所有元素均已处理）时，不变量表明整个数组有序。

   • 这正是算法设计的目标，从而证明了插入排序的正确性。

---

4. 总结

循环不变量证明方法是一种系统化的证明技巧，通常包括以下步骤：

• 初始化： 验证循环开始时不变量成立。

• 保持： 假设不变量在某次迭代成立，证明经过一次循环后仍然成立。

• 终止： 利用循环结束时的不变量，证明算法的正确性。