循环不变式 · aiwiki.page

循环不变式是关于程序状态的逻辑断言，每当执行到达循环中的某个指定位置时，它都成立；这个位置通常就在求值循环条件之前。它描述了各次迭代所保持的关系，即使个别变量的值可能发生变化。循环不变式用于证明算法的正确性，并支持程序的形式验证。不变式不必在循环体内每条中间语句处都成立。(cs.cornell.edu)

定义与证明义务

对于以下形式的循环：

while B:
    C

设 $B$ 为循环条件，也称守卫条件， $C$ 为循环体， $I$ 为候选不变式。要论证循环的正确性，需要完成三项证明义务：

**初始化：**第一次检查循环条件之前的状态满足 $I$ 。
**保持性：**如果某次迭代前 $I$ 和 $B$ 都成立，那么执行 $C$ 后， $I$ 会重新成立，前提是该次执行正常结束。
退出蕴含： $I$ 与守卫条件为假的事实 $\neg B$ 共同蕴含所需的结果。

对于 for 循环，应在执行其初始化语句后检查初始化条件；保持性的证明则要包含循环的更新步骤。过强的断言可能无法满足初始化或保持性的要求，而过弱的断言则可能无法推出所需的结果。(cs.cornell.edu)

这一推理过程是对已完成的迭代次数应用数学归纳法：初始化提供基础情形，保持性提供归纳步骤。因此，它涵盖任意有限次迭代，包括零次迭代。(cs.cornell.edu)

形式规则与终止性

在霍尔逻辑中，三元组 $\{P\}\,C\,\{Q\}$ 表示：如果命令 $C$ 从满足其前置条件 $P$ 的状态开始执行，并且正常终止，那么其最终状态满足后置条件 $Q$ 。while 循环的规则为：

\frac{\{I\land B\}\;C\;\{I\}} {\{I\}\;\texttt{while }B\texttt{ do }C\;\{I\land\neg B\}}.

前提表达了保持性；结论记录了因守卫条件为假而正常退出后可以确定的事实。初始化和逻辑蕴含关系将这条规则与循环所在程序的规格联系起来。(cs.cornell.edu)

这证明了部分正确性：如果循环终止，所声称的结果就成立。完全正确性还要求论证终止性。一种常见方法是使用循环变式，也称秩函数，其值在每次迭代中都按照某个良基序严格递减。对于取非负整数值的变式，严格递减意味着不可能进行无限次迭代。不变式表达的是被保持的性质，而变式衡量的是朝终止方向取得的进展。此外，循环体在每次迭代中也必须终止。(cs.cornell.edu)

示例：序列求和

考虑下面的伪代码，它使用精确的整数运算，对长度为 $n$ 、内容保持不变的序列 $A$ 求和：

i := 0
s := 0
while i < n:
    s := s + A[i]
    i := i + 1

一个合适的不变式是：

0\le i\le n \quad\land\quad s=\sum_{k=0}^{i-1} A[k].

它表示 $s$ 是已处理前缀的元素之和。这体现了一种常见模式：针对输入中逐步扩大的部分，描述已经完成的计算结果。(arxiv.org)

各项证明义务可以直接检查：

初始化： $i=0$ 且 $s=0$ ；空和为零。
**保持性：**如果原来的索引为 $i=j<n$ ，加上 $A[j]$ 后， $s$ 就成为前 $j+1$ 个元素的和。随后将 $i$ 加一，便恢复了所述关系。
**退出：**守卫条件为假意味着 $i\ge n$ ，而不变式给出 $i\le n$ 。因此 $i=n$ ，此时 $s$ 就是整个序列的元素之和。

变式 $n-i$ 在检查循环条件时为非负值，并且每次迭代都减一，由此可以证明终止性。注意，在两条赋值语句之间，求和关系可能暂时不成立；它会在下一次检查条件之前恢复。(dafny.org)

不变式的选择与检查

有用的不变式既要描述已经完成的工作，也要涵盖后续工作所需的约束。一种系统化方法是从后置条件出发，将其中的最终边界替换为不断变化的循环索引，前缀求和示例采用的就是这种方法。还可以添加其他子句，描述索引的取值范围、保持不变的输入值或变量之间的关系。关于不变式构造的研究对这类后置条件变换进行了分类。(arxiv.org)

验证系统可以接受显式的不变式注解。例如，在 Dafny 中，invariant 子句会生成相应的证明义务，要求断言在进入循环时成立，并在各次迭代间得到保持；另设的 decreases 子句则用于支持终止性证明。验证器在推理循环的影响时，会使用所声明的不变式。(dafny.org)

通常的退出规则适用于守卫条件变为假的情况。对于 break 等其他退出方式，需要另行推理：执行可能在不变式恢复之前就离开循环，而且此时守卫条件未必为假。因此，在循环头部成立的不变式，并不会自动成为每条可能退出路径的后置条件。(dafny.org)

参考来源

CS 2112/ENGRD 2112 Fall 2021: Loop Invariantscs.cornell.edu
Hoare: Hoare Logic, Part Ics.cornell.edu
Dafny Documentationdafny.org
Loop invariants: analysis, classification, and examplesarxiv.org