第十二讲 循环不变式¶

手工推导循环不变时的一些策略。

程序的基本事实¶

1. 变量进循环前的值
2. 循环索引：
   • 边界值
   • 更新
3. 循环控制：
   • 条件
4. 数组：
   • 数组下标的边界范围

通过基本事实推测循环不变式

不变式增强¶

1. 若某处 \(\gamma\) 需要成立但不被循环不变式支持；
2. 从该处出发到循环头/过程开始，（在某条基本路径下），计算最弱前置条件
   • 在跳出循环/进入循环的分支下，为了让后置条件成立，对循环不变式的最弱要求
3. 尽可能泛化计算得到的结果
4. 重复 2 3 步骤