loops - 确定循环不变量的最佳方法是什么？

Question

当使用形式方面来创建一些代码时，是否有确定循环不变量的通用方法，还是会根据问题完全不同？

Answer 1

已经指出，一个相同的循环可以有多个不变量，而可计算性对您不利。这并不意味着你不能尝试。

事实上，您正在寻找一个 归纳不变量 : invariant 一词也可用于在每次迭代中都为真的属性，但仅知道它在一次迭代中成立以推断它在下一次迭代中成立是不够的。如 我是归纳不变量，则 的任何结果我是不变量，但可能不是归纳不变量。

您可能正试图获得一个归纳不变量来证明在某些定义的情况(前置条件)下循环的某个属性(后置条件)。

有两种启发式方法非常有效:

从你所拥有的(先决条件)开始，然后减弱直到你有一个归纳不变量。为了直观地了解如何弱化，请应用一个或多个前向循环迭代，然后查看您所拥有的公式中哪些不再正确。

从你想要的开始(后置条件)并加强直到你有一个归纳不变量。要直观地了解如何加强，请应用一次或多次循环迭代 向后 并查看需要添加哪些内容以便推导出后置条件。

如果你想让电脑帮你练习，我可以推荐 Jessie Frama-C的C程序演绎验证插件.还有其他的，尤其是 Java 和 JML 注释，但我对它们不太熟悉。尝试你想到的不变量比在纸上工作要快得多。我应该指出，验证一个属性是归纳不变量也是不可判定的，但是现代自动证明器在许多简单的例子上做得很好。如果您决定走这条路线，请从列表中获取尽可能多的内容:Alt-ergo、Simplify、Z3。

使用可选的(安装起来有点困难)库 Apron，Jessie 还可以 infer some simple invariants automatically .