fil*_*nep 14 loops formal-methods invariants loop-invariant
当使用形式方面来创建一些代码时,是否有一种确定循环不变量的通用方法,或者它是否会根据问题完全不同？
Pas*_*uoq 19
已经指出一个相同的循环可以有几个不变量,并且可计算性对你不利.这并不意味着你不能尝试.
事实上,你正在寻找归纳不变量:单词不变量也可以用于在每次迭代时都为真的属性,但是对于它来说,它不足以知道它在一次迭代中保持它在下一个.如果我是归纳不变量,那么我的任何后果都是不变的,但可能不是归纳不变量.
您可能试图获得一个归纳不变量来证明某些特定情况(前置条件)中的循环的某个属性(后置条件).
有两种启发式方法可以很好地工作:
从你拥有的东西开始(前置条件),并削弱直到你有一个归纳不变量.为了获得如何削弱的直觉,应用一个或多个前向循环迭代,看看在你的公式中什么不再是真的.
从你想要的东西开始(后置条件)并加强直到你有一个归纳不变量.为了获得如何加强的直觉,向后应用一个或多个循环迭代并查看需要添加的内容,以便可以推导出后置条件.
如果您希望计算机在练习中为您提供帮助,我可以为Frama-C的 C程序推荐Jessie演绎验证插件.还有其他一些,尤其是Java和JML注释,但我对它们不太熟悉.如果他们在纸上工作,那么尝试你想到的不变量要快得多.我应该指出,验证属性是归纳不变量也是不可判定的,但现代自动证明器在很多简单的例子中都很有用.如果您决定走这条路线,请从列表中尽可能多地获取:Alt-ergo,Simplify,Z3.
使用可选的(并且稍微难以安装)库Apron,Jessie也可以自动推断出一些简单的不变量.
生成循环不变量实际上是微不足道的.true例如,这是一个很好的.它满足您想要的所有三个属性:
但你所追求的可能是最强的循环不变量.然而,找到最强的循环不变量有时甚至是不可判定的任务.请参阅文章可计算循环不变量的不足.