循环不变式

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

插入排序外层第 $i$ 轮开始时，可取不变式：“子数组 $A[0..i)$ 已按非降序排列，并且恰好包含输入数组原前 $i$ 个元素。”初始 $i=1$ 时单元素前缀显然满足断言；把 $A[i]$ 插入已排序前缀后，新前缀仍有序且没有增删元素，故不变式保持；退出时 $i=n$，不变式与退出条件共同说明整个数组有序且是输入的一个排列。另一方面，变式量 $n-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 循环顶部，还可覆盖后台队列、延迟工作和多层表示；终止/发布点仍须单独证明。