循环不变式 Hoare 规则

循环可以跑一百万轮，但证明不必抄写一百万次状态变换。循环不变式公理库循环不变式Loop invariant在循环初始化后成立，并在每次循环迭代后继续成立的断言。是每次回到同一控制点时仍成立的摘要；保持义务把所有可能的一轮压缩成一个通用步骤。它像在螺旋楼梯每层同一位置设置检查门：只要入口过关，而且从一扇门走到下一扇门总能恢复同一条件，就能覆盖任意有限层数。

有证明价值的不变式通常同时记录已处理部分、未处理部分与守恒量。恒真式容易初始化和保持，却往往无法在退出时推出任何有用结论；把最终后置原样当不变式又常常太强，在第一轮之前便不成立。规则把“是真的”和“足够强”分成可定位的义务。

不变式中的每个合取项承担不同角色。一个合取项可能负责防止数组越界，另一个记录结果的代数含义；保持证明要恢复全部合取，退出证明却可能只使用其中一部分。删除“看似辅助”的界限条件，有时仍能通过代数保持，却使退出状态无法被收紧到目标。

在数学整数上计算前 $n$ 个正整数之和：

i := 0
s := 0
while i < n do
    i := i + 1
    s := s + i

前置为 $n\ge 0$，取不变式

初始化后 $i=s=0$，两部分都成立。保持时设旧值为 $i,s$；guard 给 $i+1\le n$，而两条赋值后的值为 $i^{\prime }=i+1$、$s^{\prime }=s+i+1$，于是

退出时 $i\ge n$ 与 $i\le n$ 合得 $i=n$，从而 $2s=n(n+1)$。每一步都可复算，没有把目标公式当作“显然保持”。

若只保留 $2s=i(i+1)$ 而删除 $i\le n$，初始化和代数保持仍成立，但退出只给 $i\ge n$，规则本身不能推出 $i=n$。若把 body 顺序改成先 s:=s+i、再 i:=i+1，新值满足 $2s^{\prime }=i(i+1)+2i=i(i+3)$，也不再等于 $(i+1)(i+2)$；保持义务会精确捕获这次 off-by-one 改动。

不变式只要求在循环头成立；两条赋值之间代数关系可以暂时失效。带 continue 的程序必须在每条回边恢复 $I$，break 和异常则需要各自的退出后置。若把更新写成 i := i，三项部分正确性义务仍可能成立，但循环在 $i<n$ 时永不终止，说明这条规则没有隐藏的进展承诺。

循环规则把无限展开变成初始化、保持和退出三类 验证条件公理库验证条件生成Verification condition generation · VC generation按程序结构把带注解的正确性目标转换为有限逻辑义务，并以生成器可靠性连接公式有效性与程序语义。，因此是自动验证器处理用户注解的核心接口。求解器能够检查给定不变式，却不会自动保证候选足够强；抽象解释、插值和模板合成产生的候选仍须回到这三项语义义务接受检验。

若要总正确性，还需在 $I\wedge B$ 下给出落在良基集合中的变式，并证明每次循环体都终止且严格下降。数组边界、整数溢出和异常路径也必须反映在断言语言里。数学整数上的保持证明不能直接搬到会回绕的机器整数上，否则看似下降的计数器可能从最小值跳回最大值。

嵌套循环可以在内层使用依赖外层索引的不变式，再在外层把内层完整规格当作一条命令使用。直接把两个循环的所有控制点揉成一个巨型断言并非更强；分层规则能让每个不变式只承担自己循环头的事实，同时通过顺序规则传递中间后置。