循环不变式 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 和异常则需要各自的退出后置。

若把整个循环体换成 skip，保留同一 $I$，则初始化、保持和退出蕴涵仍全部成立：skip 不改状态，所以一定保持 $I$；一旦退出，$I\wedge \mathrm{\neg }B$ 仍推出求和目标。然而从 $i=s=0,n>0$ 出发，guard 永远为真，循环从不返回。这是部分正确性不保证终止的精确反例。只把原循环的 i:=i+1 改成 i:=i 而保留累加语句，则未必保持原不变式，不能用作同一个论证。

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

若要总正确性，还需在 $I\wedge B$ 下给出落在良基集合中的变式，并证明每次循环体都终止且严格下降。本例可取自然数变式 $V=n-i$：不变式给 $V\ge 0$，guard 为真时 $V>0$，原循环体执行后 $V^{\prime }=n-(i+1)=V-1$。自然数不能无限严格下降，因此循环终止；上面的 skip 版本恰好不能通过下降检查。

数组边界、整数溢出和异常路径也必须反映在断言语言里。数学整数上的保持证明不能直接搬到会回绕的机器整数上，否则看似下降的计数器可能从最小值跳回最大值。

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