Jas*_*rff 3 quantifiers dafny boogie
我在达夫尼一瘸一拐地走着，却不明白触发因素。也许因此，我编写的程序似乎给验证者带来了困难。有时我会花大量时间摆弄我的证明，试图让 Dafny/Boogie 相信它是有效的。当我让某些东西起作用时，有时验证速度很慢（这严重降低了我继续下去的能力）。
很难提出一个精确的问题，因为我不知道它是什么。但让我们从基础开始：
什么是触发器？它们什么时候使用？它们是如何推断的？一旦我理解了这一切，接下来我应该读什么？
了解触发器绝对是成为 Dafny 专家的重要组成部分！
我们最近为 Dafny 启动了一个常见问题页面，其中包括对触发器的相当广泛的描述。我建议您首先阅读常见问题解答的该部分。（这个答案的其余部分假设你已经这样做了。）
其中没有涉及的一件事是如何推断触发器。（我很快就会将此答案的编辑版本添加到常见问题解答中。）触发器实际上可能在两个不同的级别上推断：由 Dafny 或 Z3。一般来说，如果在 Dafny 级别推断触发器会更好，因为更有可能在涉及翻译到 Z3 的所有编码细节之前找到简洁的触发器。然而，如果 Dafny 无法推断出触发器，有时 Z3 仍然可以做一些有用的权宜之计。（在这种情况下，达夫尼会发出警告。）
Z3 和 Dafny 使用的推理过程在概念上非常相似。给定一个量化表达式forall x1, ..., xn :: e，推理过程尝试查找e仅涉及变量、常量和未解释的函数/谓词的子表达式，以便每个表达式都xi出现在子表达式中。例如，在表达式中
forall a, b :: P(a) && Q(a, b) ==> R(b)
该表达式Q(a, b)是一个有效的触发器，因为它提到了所有绑定变量并且不包含任何解释函数。另一个有效的触发器是表达式集{P(a), R(b)}。一个触发器或另一个（或两者）哪个更好取决于上下文。通常，Dafny 会推断并使用所有有效的、最通用的触发器，因此在这种情况下，它将选择Q(a, b)和{P(a), R(b)}。
一般来说，Dafny 的触发器推断通过查看 的所有子表达式来枚举所有有效触发器e。然后，Dafny 过滤掉严格来说不如另一个有效触发器通用的触发器。Dafny 选择所有剩余的触发器。
如需补充阅读，我推荐 Detlefs、Nelson 和 Saxe 撰写的论文《简化：用于程序检查的定理证明者》。Simplify 是一个早期的 SMT 求解器，它开创了启发式使用触发器来处理量词的先河。上述论文的第 5 节详细描述了该方法的技术细节。