控制流图
入口和出口
入口 ---> 判断 ---> 出口
| |
| |
|____|
对于每个判断,有两个入口: 第一次入口 , 后续的入口
对于每个判断,有两个出口:exit跳出循环, 继续循环
1 第一次入口满足断言
2 每次判断继续循环满足断言
我们可以得出结论:
出口必然满足断言
- 判断不改变断言
- 每个入口都满足断言
可以推出exit满足断言
如何形式化证明
如果证明,或者如何抽象出这个证明或者我们找到一个同构的问题
循环不变式核心是 满足约束:
1 初始化条件满足断言
2 每次迭代后满足断言
3 循环是可计算的(不是死循环)
其实3只是为了不会死循环,核心条件是1和2