我一直在 Dafny 中一瘸一拐地走着，不了解触发器。也许结果是，我编写的程序似乎让验证者很难受。有时我会花费大量时间摆弄我的证明，试图让 Dafny/Boogie 相信它是有效的；当我得到一些工作时，有时验证速度很慢（这严重降低了我继续的能力）。
很难问一个准确的问题，因为我不知道我不知道它是什么。但让我们从基础开始：
什么是触发器？它们什么时候使用？它们是如何推断的？一旦我理解了所有这些，我接下来应该读什么？
【问题讨论】：
标签： quantifiers dafny boogie
了解触发器绝对是成为 Dafny 专家的重要部分！
我们最近为 Dafny 启动了 frequently asked questions page，其中包含相当广泛的触发器描述。我建议您从阅读常见问题解答的那部分开始。 （此答案的其余部分假设您已经这样做了。）
其中未涉及的一件事是如何推断触发器。 （我将很快将这个答案的编辑版本添加到常见问题解答中。）实际上可能在两个不同的级别上推断出触发器：Dafny 或 Z3。一般来说，最好在 Dafny 级别推断触发器，因为在涉及到从翻译到 Z3 的所有编码细节之前，更有可能找到一个简洁的触发器。但是，如果 Dafny 无法推断出触发器，有时 Z3 仍然可以做一些有用的事情作为权宜之计。 （在这种情况下，Dafny 会发出警告。）
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)} 的set。一个触发器或另一个（或两者）更好取决于上下文。通常，Dafny 会推断并使用所有有效的、最通用的触发器，因此在这种情况下，它将同时选择 Q(a, b) 和 {P(a), R(b)}。
通常，Dafny 的触发器推断通过查看e 的所有子表达式来枚举所有有效触发器来工作。然后，Dafny 过滤掉严格来说不如另一个有效触发器通用的触发器。 Dafny 选择所有剩余的触发器。
如果想进一步阅读，我推荐 Detlefs、Nelson 和 Saxe 的论文 Simplify: A Theorem Prover for Program Checking。 Simplify 是早期的 SMT 求解器，它开创了启发式使用触发器来处理量词的方法。上述论文的第 5 节详细描述了该方法。
【讨论】：