Dafny 无法证明简单的存在量词

Question

这可能是一个非常愚蠢的问题，但这里是:

为什么 Dafny 可以做到这一点:

var arr := new int[2];
arr[0], arr[1] := -1, -2;
assert exists k :: 0 <= k < arr.Length && arr[k] < 0;

但不是这个:

var arr := new int[2];
arr[0], arr[1] := -1, 2;
assert exists k :: 0 <= k < arr.Length && arr[k] < 0;

我在我的大程序中追踪到一个错误。我敢肯定这是我忽略的小事，但我很感激你的帮助!

Answer 1

这个微妙的问题是由于处理堆更新的顺序造成的。首先，让我们简化示例，因为它不特定于正数和负数。

type T
predicate P(t: T)

method ThisFails(t0: T, yes: T, no: T) requires P(yes) && !P(no) {
  var arr := new T[2](_ => t0);
  arr[0] := yes;
  arr[1] := no;
  assert exists k :: 0 <= k < arr.Length && P(arr[k]); // FAILS [:(]
}

翻转两个数组修改可以解决问题:

type T
predicate P(t: T)

method ThisFails(t0: T, yes: T, no: T) requires P(yes) && !P(no) {
  var arr := new T[2](_ => t0);
  arr[1] := no;  // Different order
  arr[0] := yes; // Different order
  assert exists k :: 0 <= k < arr.Length && P(arr[k]); // SUCCEEDS [?!]
}

为什么这些示例的行为不同？

理解正在发生的事情的关键是思考如何arr[ idx ] := value ]影响验证状态。当您分配给一个数组时，Dafny 了解到:

• 数组变了
• 职位idx映射到 value在新数组
• 旧和新数组之间其他位置不变

所以在上面第一个(损坏的)代码示例中的两次赋值之后，我们有

• 数组变了
• 职位0映射到 yes在中间数组
• 职位1映射到 no在final数组中

相比之下，在上面第二个(有效的)代码示例中的两次赋值之后，我们有:

• 数组变了
• 职位1映射到 no在中间数组
• 职位0映射到 yes在final数组中

注意哪个事实谈论中间数组，哪个事实谈论最终数组。在损坏的示例中我们知道 arr[0] == yes在中间数组中。在工作示例中我们知道 arr[0] == yes在 final 数组中。

当然，我们可以证明最后的数组有arr[0] == yes ，但在第二个(损坏的)损坏示例中默认情况下我们不知道它。

为什么这很重要？

量词的证明是这样的:

1. 否定断言:它变成forall k | 0 <= k < arr.Length :: !P(arr[k])
2. 通过实例化量词来寻找矛盾。

如果将鼠标悬停在量词上，您将看到 Selected triggers: {arr[k]}这意味着 Dafny 将“学习”!P(arr[k])任何时候它已经知道关于 arr[ 的一些 k ]对于一些 k .

重要的是，量词指的是数组的最终状态!因此，不使用关于数组的中间状态的事实。

在上面的破例子中，我们了解了关于最终数组的以下内容，这还不足以推导出矛盾并完成证明。

• arr[1] == no (来自上次作业，因此 !P(arr[1]) )
• !P(arr[1]) (来自量词)

在上面的工作示例中，我们了解到有关最终数组的以下内容，足以导出矛盾并完成证明。

• arr[0] == yes (来自上次作业，因此 P(arr[0]) )
• !P(arr[0]) (来自量词)

在损坏的情况下，可以通过声明 assert arr[0] == yes; 来解决问题。 ，这很容易证明，并告诉我们我们需要关于最终数组的事实。

结语

我们可以使用标签使中间状态显式化:

method ThisFails(t0: T, yes: T, no: T) requires P(yes) && !P(no) {
  var arr := new T[2](_ => t0);
  label initial:
    arr[0] := yes;
  label intermediate:
    arr[1] := no;
  label final:
    assert true;
  assert exists k :: 0 <= k < arr.Length && P(arr[k]); // FAILS
}

然后，添加断言 assert old@intermediate(arr[0]) == old@final(arr[0]); 就足够了确认这部分数组没有被修改。

查看问题的另一种方法是使用序列重现问题:

method ThisFails(t0: T, yes: T, no: T) requires P(yes) && !P(no) {
  var sq := [t0, t0];
  var sq0 := sq[0 := yes];
  var sq1 := sq0[1 := no];
  // We know sq0[0] == yes, but not sq1[0] == yes
  // assert sq1[0] == yes; // Adding this fixes the issue
  assert exists k :: 0 <= k < |sq1| && P(sq1[k]); // FAILS
}