当使用形式方面来创建一些代码时，是否有确定循环不变量的通用方法，或者它会根据问题完全不同？
问问题
28780 次
5 回答
21
已经指出，同一个循环可以有多个不变量，而可计算性对你不利。这并不意味着你不能尝试。
事实上，您正在寻找一个归纳不变量：这个词也可以用于在每次迭代中都为真的属性，但是仅仅知道它在一次迭代中成立还不足以推断它在下一个。如果I是归纳不变量，则I的任何结果都是不变量，但可能不是归纳不变量。
您可能正试图获得一个归纳不变量来证明在某些定义的情况下（前置条件）循环的某个属性（后置条件）。
有两种启发式方法效果很好：
从你所拥有的（前提条件）开始，然后减弱直到你有一个归纳不变量。为了直观地了解如何削弱，应用一个或几个前向循环迭代，看看你所拥有的公式中什么不再是正确的。
从你想要的（后置条件）开始并加强，直到你有一个归纳不变量。为了直观地了解如何加强，向后应用一个或几个循环迭代，看看需要添加什么，以便可以推断出后置条件。
如果你想让电脑帮你练习，我可以推荐Frama-C的C程序的Jessie演绎验证插件。还有其他一些，尤其是 Java 和 JML 注释，但我对它们不太熟悉。尝试你想到的不变量比在纸上工作要快得多。我应该指出，验证一个属性是一个归纳不变量也是不可判定的，但是现代自动证明器在许多简单的例子上都做得很好。如果您决定走这条路，请从列表中获取尽可能多的信息：Alt-ergo、Simplify、Z3。
借助可选的（且安装难度稍大）库 Apron，Jessie 还可以自动推断一些简单的不变量。
于 2010-08-05T11:25:59.910 回答
9
生成循环不变量实际上很简单。true是一个很好的例子。它满足您想要的所有三个属性：
- 它在循环进入之前保持
- 它在每次迭代后保持
- 它在循环终止后保持
但是你所追求的可能是最强的循环不变量。然而，找到最强的循环不变量有时甚至是一项无法确定的任务。请参阅文章Inadequacy of Computable Loop Invariants。
于 2010-06-10T05:33:19.863 回答
2
我认为自动化这一点并不容易。来自维基：
由于循环和递归程序的基本相似性，用不变量证明循环的部分正确性与通过归纳证明递归程序的正确性非常相似。实际上，循环不变量通常是人们必须证明的递归程序的归纳属性，该递归程序等效于给定的循环。
于 2010-05-29T14:47:20.977 回答
1
我在博客中写过关于编写循环不变量的文章，请参阅验证循环第 2 部分。证明循环正确所需的不变量通常包括 2 个部分：
- 循环终止时预期的状态的概括。
- 需要额外的位来确保循环体的格式正确（例如，数组索引在边界内）。
(2) 直截了当。要导出 (1)，请从表示终止后所需状态的谓词开始。它可能在某些数据范围内包含“forall”或“exists”。现在更改“forall”或“exists”的边界，以便（a）它们依赖于循环修改的变量（例如循环计数器），以及（b）这样当第一次进入循环时不变量是微不足道的（通常通过使“forall”或“exists”的范围为空）。
于 2011-02-10T01:20:39.003 回答
0
有许多用于查找循环不变量的启发式方法。关于这方面的一本好书是 Ed Cohen 的“1990 年代的编程”。它是关于如何通过手动操作后置条件来找到一个好的不变量。示例是：用变量替换常量，加强不变量，...
于 2010-08-06T21:39:19.073 回答