如何确定循环不变式是最佳方法？

Question

如何确定循环不变式是最佳方法？

loopsinvariantsformal-methodsloop-invariant

17

在使用正式方面来创建代码时，是否有一种通用的方法来确定循环不变量，还是这将完全取决于问题而有所不同？

- filinep

5个回答

10

生成循环不变式其实非常简单。true是一个好的例子。它满足你想要的所有三个属性：

在进入循环之前它成立。
在每次迭代后它仍然成立。
在循环终止后它仍然成立。

但是，你可能需要的是最强的循环不变式。然而，找到最强的循环不变式有时甚至是一个不可判定的任务。请参阅文章《可计算循环不变式的不充分性》。

- aioobe

"True" 是弱的。我认为你的意思是“你想要最强的循环不变量”。你的回答提出了一个很好的观点，但我认为通常需要“任何归纳不变量足够强大以证明所考虑的属性”。最强的循环不变量可能不存在（如果有无限个变量，则将“x' = x”添加到不变量中会构建一个更强的不变量），并且可能难以处理。 - Pascal Cuoq

关于“最弱”，你当然是对的。我搞混了！（我认为它是“真实的，因为它不意味着任何事情”）。回答已更新。不过，你的第二个观点似乎有些牵强。你是说它不存在，因为需要无限的空间来写下它吗？ - aioobe

嗯，在大多数逻辑中，一个公式是一组有限的符号组合，我认为如果你允许无限的符号组合，即使限制自己在可以有限地描述的正则组合中，一些元定理也可能不成立。所以你必须小心。撇开这个细节不谈（例如，在ACSL中，你可以声明有限子句中无限变量的不变性），我的观点是最强的不变量可能比必要的更复杂。 - Pascal Cuoq

这是一个很好的观点。最强的循环不变量有时超出了人们的需求。同意。尽管如此，OP和我的答案在技术上都没有涉及公式。你是唯一提到这种表示方法的人。;) - aioobe

也许一个改进的方法是将其称为“归纳循环不变量，足以证明正确性”（相对于所需的前置条件和后置条件）。 - 0 _

2

我认为自动化这个过程并不容易。来自维基百科的解释：

由于循环和递归程序的基本相似性，通过不变式证明循环的部分正确性与通过归纳证明递归程序的正确性非常相似。实际上，循环不变式通常是等效于给定循环的递归程序所必须证明的归纳属性。

- František Žiačik

谢谢，我不想自动化它，这只是为了笔试练习，我需要找到循环不变量。我想这只需要多练习就可以了。 - filinep

1

有许多启发式方法可以找到循环不变量。其中一本好书是Ed Cohen的“Programming in the 1990s”。它介绍了如何通过手动操作后置条件来找到一个好的不变量。例如：用变量替换常量，加强不变量等。

- xpmatteo

1

我在我的博客中写过关于编写循环不变式的文章，可以参考验证循环第二部分。证明循环正确所需的不变式通常包括两个部分：

当循环终止时期望的状态的概括。
额外的位，用于确保循环体是良好形式的（例如数组索引在边界内）。

(2)很简单。要得出(1)，从表达所需状态的谓词开始。很可能它包含一些数据范围上的“forall”或“exists”。现在更改“forall”或“exists”的边界，使(a)它们依赖于循环修改的变量（例如循环计数器），并且(b)使不变式在循环首次进入时显然为真（通常通过使“forall”或“exists”的范围为空来实现）。

- dc42

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Pascal Cuoq · Accepted Answer

已经指出一个循环可以有多个不变量，并且可计算性不支持你。这并不意味着你不能尝试。

实际上，你正在寻找归纳不变量：该词也可用于每次迭代都为真但仅知道它在一个迭代中成立就无法推断它在下一个迭代中成立的属性。如果 I 是归纳不变量，则 I 的任何结果都是不变量，但可能不是归纳不变量。

你可能正在尝试获得一个归纳不变量来证明某些定义情况（前提条件）下循环的某个属性（后置条件）。

有两个启发式方法非常有效：

- 从现有内容（前提条件）开始，逐渐削弱直到获得归纳不变量。为了获得如何削弱的直觉，请应用一个或多个向前的循环迭代，并查看您拥有的公式中哪些不再成立。 - 从所需内容（后置条件）开始加强，直到获得归纳不变量。为了获得加强的直觉，请向后应用一个或多个循环迭代，并查看需要添加什么才能推导出后置条件。

如果您希望计算机在实践中帮助您，我可以推荐Frama-C的C程序Jessie演绎验证插件。还有其他一些插件，特别是针对Java和JML注释的插件，但我不太熟悉它们。尝试想到的不变量比在纸上计算它们要快得多。我应该指出，验证属性是否为归纳不变量也是不可判定的，但现代自动证明器在许多简单的例子中表现出色。如果您决定选择这条路，请尽可能从列表中获取：Alt-ergo、Simplify、Z3。

使用可选的（并且稍微难以安装的）Apron库，Jessie还可以自动推断一些简单的不变量。