循环不变式

循环不变式是每个迭代边界都为真的状态摘要。它把“循环可能执行任意多轮”压缩成一次归纳：先证明起点成立，再证明任意一轮都保持。一个有证明价值的不变式通常同时描述已经处理的部分、尚未处理的部分，以及二者之间仍保持的关系。太弱的不变式虽然为真，却无法在退出时推出目标；太强的断言则可能根本无法初始化或保持。它不是对最终结果的愿望，而是每条循环路径执行后都必须重新建立的事实。

插入排序先对长度小于 $2$ 的数组直接返回。其余情形记输入快照为 $A_0$，固定数组长度为 $n\ge 2$，外层从 $i=1$ 开始，在 $i<n$ 时把 $A[i]$ 插入前缀，再令 $i\leftarrow i+1$。可取以下完整不变式：$1\le i\le n$；$A[0..i)$ 非降序，且按重数恰好包含 $A_0[0..i)$ 的元素；未处理后缀 $A[i..n)$ 逐项等于 $A_0[i..n)$。

初始化时，单元素前缀已有序，整个数组仍等于输入快照。保持时，后缀条件保证待插入的 $A[i]$ 正是原输入的 $A_0[i]$；把前缀中比它大的元素依次右移，再填入该元素，便得到有序且重数正确的前 $i+1$ 项。更后的后缀没有被修改，所以 $i$ 加一后重新满足完整断言。退出时由 $i\le n$ 和 $i\nless n$ 得 $i=n$，整个数组于是有序且是输入的一个排列。

后缀条件承担实际的归纳义务。例如原输入为 $[2,1]$，状态 $i=1,A=[2,99]$ 的首项满足原前缀的有序与重数条件，但插入 $99$ 后得不到原输入前两项的排列。它不可从正常初始化到达，却属于“只约束前缀”的断言所允许的状态；因此那条较弱断言不足以独立满足本页要求的任意状态保持。

终止还需另计：外层变式量 $n-i$ 每轮下降一且非负；插入内部的左移指针也逐次减小，至多越过前缀的全部 $i$ 个位置，所以每次循环体本身会终止。两层下降论证合起来才给出总正确性。

“数组最终会有序”不是有效不变式，因为循环中未必成立。只证明保持而忘记终止也不能得到总正确性；若循环可能无限执行，不变式最多证明部分正确性。修改多个变量时必须检查所有会回到循环头的分支，包括 continue；若异常直接离开循环，则应另行证明异常后置条件，只有被循环体捕获并继续迭代的异常路径才必须重建 $I$。

循环不变式用于排序、图遍历、动态规划和数据结构操作的正确性证明。

它是 算法正确性理路算法正确性Algorithm correctness · Partial and total correctness所有合法执行都符合规格，并在完全正确时保证终止。 的基本证明工具，其初始化与保持正是一种 数学归纳法理路数学归纳法Mathematical induction · Weak induction由基例和从 n 到 n+1 的归纳步推出性质对全部自然数成立。。更一般的归纳不变式理路不变式与归纳不变式Invariant · Inductive invariant · Strengthened invariant区分所有可达状态上成立的性质与由初始性和一步闭包直接证明的归纳不变式。把循环头看作状态集合上的切点：初始化对应初始状态纳入集合，保持对应循环回边下封闭；这一区分也解释了为何所有可达状态都满足的真性质，未必已经是可直接归纳证明的不变式。二分搜索的候选区间、图遍历的已访问集合和流算法的可行性都可写成不变式；在程序逻辑中，Hoare 三元组理路Hoare 三元组Hoare triple断言若前置条件成立且程序终止，则后置条件成立的 {P}C{Q} 形式。的 while 规则把“初始化、保持、退出推出后置条件”明确拆成独立验证义务，SMT 验证理路基于 SMT 的软件验证SMT-based software verification · SMT-aided program verification将路径条件、验证条件和理论约束交给 SMT 求解器，以模型或不可满足证明支持软件正确性判断。可以求解生成的逻辑条件，却不会替代不变式的语义选择。

高级动态结构常需跨多次公开操作的不变量。去摊还化理路去摊还化Deamortization把批量工作拆成有截止期的微步，以顺序动态数组的读、写、追加证明权威槽不变量、迁移期限和逐操作最坏界。在迁移期同时维护新旧版本与复制进度；Link–Cut Tree理路Link–Cut TreeLink-cut tree以 preferred-path 分解和辅助伸展树维护动态森林，在对数摊还时间内支持换根、连边、断边与路径聚合。区分 represented forest 和 auxiliary splay，并在 access 后恢复 preferred-path 表示；Buffer Tree理路Buffer Treebuffer tree · 缓冲树在高扇出树节点积累操作并批量下推，以排序量级 I/O 支持批量动态操作。允许更新暂存在缓冲区，却保证批量下推后查询语义。它们说明不变量不只写在单个 for 循环顶部，还可覆盖后台队列、延迟工作和多层表示；终止/发布点仍须单独证明。