如何在 Dafny 中验证前置/后置条件答案

【问题标题】：How to verify pre/post conditions in Dafny如何在 Dafny 中验证前置/后置条件
【发布时间】：2020-04-07 22:24:45
【问题描述】：

我是达夫尼的新手。我正在尝试一些示例以更好地理解。

这是我到目前为止编写的代码示例， 编辑： https://rise4fun.com/Dafny/6mOt 我不确定如何完全满足这些前置/后置条件。我尝试了一些东西，但没有帮助。任何帮助，将不胜感激。

谢谢！

【问题讨论】：

我认为您需要提供更具体的问题或展示实现这些循环的一些努力，然后我们才能为您提供帮助。我们怎么知道这不是作业？
@MatthiasSchlaipfer：好的，现在我已经更新了代码 sn-p。我还想知道 dafny 中是否有一些调整数组大小的内置函数？还是唯一的方法是创建一个新实例？
不，目前没有这样的功能。当然，可以实现一个辅助方法，也许只是一个{:extern} 方法存根，用于已经内置到 Dafny 的一种目标语言中的这种库方法，添加前置/后置条件将是一个不错的选择。谁知道呢，也许在某个时候会添加一个到github.com/dafny-lang/libraries

标签： dafny

【解决方案1】：

Dafny 不会推断出任何不变量，因此您需要添加它们。特别是如果您已经知道后置条件并且您的循环位于方法的末尾，则更容易找到它。有时只需用循环计数器替换您正在迭代的数组的长度就足够了。然后，在循环结束时，当i >= n时，你可以认为不变量变成了后置条件。

在你的情况下，它让我走得很远，但需要一些调整。您需要添加的不变量之一是

invariant forall j : int :: 0 <= j < i && j < m ==> cells[j] == copy[j]

我把另一个留给你。

【讨论】：