这可能是一个非常愚蠢的问题，但这里是：
为什么 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;
我已经在我的大程序中追踪到一个错误。我敢肯定这是我忽略的小事，但我很感激你的帮助！
【问题讨论】：
标签： dafny
有趣的问题。我不确定！也许其他人可以参与更深入的调查。
我只想提一下，这个问题与触发器有关。任何时候你要求 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] 完全没有。只要我们提到它，我们就可以说些愚蠢的话。
【讨论】：