dafny - Dafny 中的琐碎断言违规

Question

为什么 Dafny 声称这个简单的断言可能被违反了？

var b := new int[2];
b[0],b[1] := 1, -2;
assert exists k | 0 <= k < b.Length :: (b[k] == 1 || b[k] == -1);

标签： dafny

Answer 1

这与 Dafny 处理存在量词的方式有关。它（几乎）永远不会“猜测”你的价值。相反，Dafny 使用句法启发法（称为“触发器”）从上下文中尝试某些值。

在您的断言中，触发器是b[k]，这意味着 Dafny 只会尝试明确提及k表达式的值。b[k]

k因此，修复断言的一种方法是通过添加断言来明确提及 的正确值

assert b[0] == 1;

甚至

assert b[0] == 1 || b[0] == -1

---

这与这个问题有些相关。

有关触发器的更多信息，请参见此答案。