1

将整数数组的负元素复制到另一个数组的方法具有以下属性：结果中的元素集是原始数组中元素的子集，在复制过程中保持不变。

下面代码中的问题是，只要我们在结果数组中写入一些内容，Dafny 就会不知何故忘记原始集合没有改变。如何解决这个问题？

method copy_neg (a: array<int>, b: array<int>)
  requires a != null && b != null && a != b
  requires a.Length == b.Length
  modifies b
{
  var i := 0;
  var r := 0;
  ghost var sa := set j | 0 <= j < a.Length :: a[j];
  while i < a.Length
    invariant 0 <= r <= i <= a.Length
    invariant sa == set j | 0 <= j < a.Length :: a[j]
  {
    if a[i] < 0 {
      assert sa == set j | 0 <= j < a.Length :: a[j]; // OK
      b[r] := a[i];
      assert sa == set j | 0 <= j < a.Length :: a[j]; // KO!
      r := r + 1;
    }
    i := i + 1;
  }
}

编辑

按照James Wilcox 的回答，用序列上的谓词替换集合的包含是最有效的。

这是完整的规范（对于具有不同元素的数组）。后置条件必须在循环不变量中进行一些详细说明，并且在循环中间保留一个愚蠢的断言，但是所有幽灵变量都消失了，这很棒。

method copy_neg (a: array<int>, b: array<int>)
  returns (r: nat)
  requires a != null && b != null && a != b
  requires a.Length <= b.Length
  modifies b
  ensures 0 <= r <= a.Length
  ensures forall x | x in a[..] :: x < 0 <==> x in b[..r]
{
  r := 0;
  var i := 0;
  while i < a.Length
    invariant 0 <= r <= i <= a.Length
    invariant forall x | x in b[..r] :: x < 0
    invariant forall x | x in a[..i] && x < 0 :: x in b[..r]
  {
    if a[i] < 0 {
      b[r] := a[i];
      assert forall x | x in b[..r] :: x < 0;
      r := r + 1;
    }
    i := i + 1;
  }
}
4

1 回答 1

1

这确实令人困惑。我将在下面解释为什么 Dafny 难以证明这一点，但首先让我给出一些方法来让它通过。

第一个解决方法

使证明通过的一种方法是forall在该行之后插入以下语句b[r] := a[i];。

forall x | x in sa
  ensures x in set j | 0 <= j < a.Length :: a[j]
{
  var j :| 0 <= j < a.Length && x == old(a[j]);
  assert x == a[j];
}

该forall声明是一个证明sa <= set j | 0 <= j < a.Length :: a[j]。我将在下面回到为什么这有效。

第二种解决方法

一般来说，在 Dafny 中推理数组时，最好使用a[..]语法将数组转换为数学序列，然后使用该序列。如果你真的需要使用这组元素，你可以使用set x | x in a[..]，而且你会比使用set j | 0 <= j < a.Length :: a[j].

系统地替换set j | 0 <= j < a.Length :: a[j]withset x | x in a[..]会导致您的程序进行验证。

第三个解决方案

弹出一个级别来指定您的方法，似乎您实际上不需要提及所有元素的集合。相反，你可以说“每个元素b都是a”之类的话。或者，更正式地说forall x | x in b[..] :: x in a[..]。这对于您的方法来说不是一个有效的后置条件，因为您的方法可能不会填写所有b. 由于我不确定您的其他限制是什么，我将把它留给您。

解释

Dafny 的具有 type 元素的集合A被转换为 Boogie maps [A]Bool，其中一个元素映射为 true 如果它在集合中。诸如set j | 0 <= j < a.Length :: a[j]被翻译为定义涉及存在量词的布吉地图的理解。这种特殊的理解转化为映射到的x映射

exists j | 0 <= j < a.Length :: x == read($Heap, a, IndexField(j))

其中read表达式是 的 Boogie 翻译a[j]，特别是使堆显式化。

因此，要证明一个元素在推导式定义的集合中，Z3 需要证明一个存在量词，这很难。Z3 使用触发器来证明此类量词，Dafny 告诉 Z3read($Heap, a, IndexField(j))在尝试证明此量词时使用触发器。事实证明这不是一个很好的触发器选择，因为它提到了堆的当前值。因此，当堆发生变化时（即更新后b[r]），触发器可能不会触发，并且您会得到一个失败的证明。

Dafny 允许您使用{:trigger}属性自定义它用于集合推导的触发器。不幸的是，在 Dafny 级别没有很好的触发器选择。然而，这个程序在 Boogie/Z3 级别的一个合理的触发器将是 just IndexField(j)（尽管这对于一般的此类表达式来说可能是一个不好的触发器，因为它过于笼统）。如果 Dafny 没有另外说明，Z3 本身会推断出这个触发器。{:autotriggers false}你可以说，像这样，达芙妮让开

invariant sa == set j {:autotriggers false} | 0 <= j < a.Length :: a[j]

这个解决方案不能令人满意，并且需要对 Dafny 的内部结构有详细的了解。但是既然我们已经理解了它，我们也可以理解我提出的其他解决方法。

对于第一个解决方法，证明通过，因为forall语句提及a[j]，这是触发器。这使 Z3 成功地证明了存在性。

对于第二种解决方法，我们简化了集合理解表达式，使其不再引入存在量词。相反，理解set x | x in a[..]被转换为映射到的x映射

x in a[..]

（忽略如何a[..]翻译的细节）。这意味着 Z3 永远不必证明存在性，因此其他非常相似的证明也会通过。

第三种解决方案出于类似的原因起作用，因为它不使用任何理解，因此没有有问题的存在量词/

于 2017-09-11T01:05:09.800 回答