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

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

• 阵列已更改
• 在中间数组中将1映射到no的位置
• 在最终数组中定位0映射到yes

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

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

为什么这很重要？

量词的证明是这样的：

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

如果你将鼠标悬停在量词上，你会看到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
}

Answer 2

有趣的问题。我不确定！也许其他人可以插话进行更深入的调查。

让我提一下，这个问题与触发器有关。每当你要求Dafny证明一个存在时，你必须明白它(和底层求解器Z3)使用句法启发式。它查看量词的主体并尝试找到"触发器"或模式。选择触发器后，它只会猜测与触发器匹配的 k 值。

在您的特定示例中，触发器是arr[k]。因此，Dafny只会尝试猜测k的值，其中arr[k]已经在程序的其他地方提到过。

同样重要的是要了解数组是堆分配的，并且"在程序其他地方提到"子句主要适用于当前堆。该程序提到了arr[0]和arr[1]，但它提到了前一堆中的那些，在第 2 行的赋值语句之前。

综上所述，我实际上更惊讶Dafny可以证明你的第一个例子中的断言，而不是我不能证明第二个例子。

最后，让我指出，一旦你理解了触发器是Dafny理解量词的方式，就很容易手动哄骗Dafny来证明第二个断言：只需提到arr[k]，因为你知道k的值是正确的。换句话说，在程序中的现有断言之前插入此行：

assert arr[0] < 0;

请注意，我们断言arr[0]小于 0 实际上并不重要。重要的是我们根本没有提到arr[0]。我们可以说一些愚蠢的话，只要我们提到它。