1

在阅读了 Dafny 入门：指南之后，我决定创建我的第一个程序：给定一个整数序列，计算其元素的总和。但是，我很难让 Dafny 验证该程序。

function G(a: seq<int>): int
  decreases |a|
{
  if |a| == 0 then 0 else a[0] + G(a[1..])
}

method sum(a: seq<int>) returns (r: int)
  ensures r == G(a)
{
  r := 0;
  var i: int := 0;
  while i < |a|
    invariant 0 <= i <= |a|
    invariant r == G(a[0..i])
  {
    r := r + a[i];
    i := i + 1;
  }
}

我明白了

stdin.dfy(12,2): Error BP5003: A postcondition might not hold on this return path.
stdin.dfy(8,12): Related location: This is the postcondition that might not hold.
stdin.dfy(14,16): Error BP5005: This loop invariant might not be maintained by the loop.

我怀疑 Dafny 需要一些“帮助”来验证程序（可能是引理？），但我不知道从哪里开始。

4

1 回答 1

1

这是您的程序可以验证的版本。

有两件事情需要解决：证明后置条件在循环之后，以及证明循环不变量被保留。

后置条件

Dafny 需要一个提示，试图证明它可能会有所帮助a == a[..|a|]。断言相等性足以完成这部分证明：Dafny 自动证明相等性并使用它来证明循环不变量的后置条件。

这是一种常见的模式。您可以尝试通过在 Dafny 中“手动”进行证明来查看困扰 Dafny 的问题，方法是做出各种您将用来在纸上向自己证明的断言。

循环不变量

这个有点复杂。我们需要证明更新r和递增i保留r == G(a[..i]). 为此，我使用了一个calc语句，让我们通过一系列中间步骤来证明相等性。calc（如果您愿意，可以通过断言所有相关的等式以及 . 内的任何断言来证明这些事情，calc但我认为calc更好。）

我将calc声明放在更新r和i发生之前。我知道更新发生后，我需要证明和r == G(a[..i])的更新值。因此，在更新发生之前，证明未更新的值就足够了。我的陈述以.rir + a[i] == G(a[..i+1])calcr + a[i]G(a[..i+1])

首先，通过进入循环时的循环不变量，我们知道r == G(a[i])对于当前值。

接下来，我们要把a[i]里面的G. 这个事实并不完全是微不足道的，所以我们需要一个引理。我选择证明一些比必要的更一般的东西，即G(a + b) == G(a) + G(b)对于任何整数序列a和b. 我称之为引理G_append。下面讨论它的证明。现在，我们只是使用它来获取a[i]内部作为单例序列。

最后一步calc是合并a[0..i] + [a[i]]成a[0..i+1]. 这是另一个序列可扩展性事实，因此需要明确声明。

这完成了calc，这证明了不变量被保留。

引理

在 上通过归纳证明G_append收益a。a == []自动处理的基本情况。在归纳的情况下，我们需要证明G(a + b) == G(a) + G(b)，假设 的任何子序列的归纳假设a。我calc为此使用了另一种说法。

从 开始G(a + b)，我们首先扩展 的定义G。接下来，我们注意到(a + b)[0] == a[0]由于a != []. 类似地，我们有(a + b)[1..] == a[1..] + b，但由于这是另一个序列外延事实，它必须被显式断言。最后，我们可以使用归纳假设（由 Dafny 自动调用）来证明G(a[1..] + b) == G(a[1..]) + G(b).

于 2017-07-29T07:31:24.157 回答