循环不变式

循环不变式是程序验证中的核心概念，用于证明循环的正确性。

定义

在循环执行过程中始终保持为真的性质。

三个阶段

1. 初始化：循环开始前不变式成立
2. 保持性：每次迭代后不变式仍然成立
3. 终止性：循环结束时不变式结合终止条件可推出目标性质

生成方法

• 模板法
• 抽象解释
• 机器学习辅助