在使用正式方面来创建代码时,是否有一种通用的方法来确定循环不变量,还是这将完全取决于问题而有所不同?
在使用正式方面来创建代码时,是否有一种通用的方法来确定循环不变量,还是这将完全取决于问题而有所不同?
使用可选的(并且稍微难以安装的)Apron库,Jessie还可以自动推断一些简单的不变量。
生成循环不变式其实非常简单。true
是一个好的例子。它满足你想要的所有三个属性:
但是,你可能需要的是最强的循环不变式。然而,找到最强的循环不变式有时甚至是一个不可判定的任务。请参阅文章《可计算循环不变式的不充分性》。
我认为自动化这个过程并不容易。来自维基百科的解释:
由于循环和递归程序的基本相似性,通过不变式证明循环的部分正确性与通过归纳证明递归程序的正确性非常相似。实际上,循环不变式通常是等效于给定循环的递归程序所必须证明的归纳属性。
有许多启发式方法可以找到循环不变量。其中一本好书是Ed Cohen的“Programming in the 1990s”。它介绍了如何通过手动操作后置条件来找到一个好的不变量。例如:用变量替换常量,加强不变量等。