我一直在Dafny一瘸一拐地走着，不了解触发器。也许正因为如此，我编写的程序似乎给验证者带来了困难。有时我会花大量时间摆弄我的证明，试图说服 Dafny/Boogie 它是有效的;当我得到一些工作时，有时验证速度很慢(这严重降低了我继续的能力(。
很难问一个准确的问题，因为我不知道它是什么，我不知道。但让我们从基础知识开始：
什么是触发器？何时使用？它们是如何推断的？一旦我理解了所有这些，我接下来应该读什么？
了解触发因素绝对是成为Dafny专家的重要组成部分！
我们最近为 Dafny 开设了一个常见问题页面，其中包括对触发器的相当广泛的描述。我建议您从阅读常见问题解答的这一部分开始。(本答案的其余部分假设您已经这样做了。
这里没有涉及的一件事是如何推断触发器。(我将很快将此答案的编辑版本添加到常见问题解答中。触发器实际上可能在两个不同的级别推断：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)}集。一个触发器还是另一个(或两个(更好取决于上下文。通常，Dafny 会推断并使用所有有效的、最通用的触发器，因此在这种情况下，它会同时选择Q(a, b)和{P(a), R(b)}。
通常，Dafny 的触发器推理的工作原理是通过查看e的所有子表达式来枚举所有有效触发器。然后，Dafny 会过滤掉严格不如另一个有效触发器通用的触发器。Dafny 选择所有剩余的触发器。
对于其他阅读，我推荐Detlefs，Nelson和Saxe的论文Simplify：A Theorem Prover for Program Check。简化是早期的 SMT 求解器，它开创了启发式使用触发器来处理量词的先河。上述文件第5节从技术细节上详细描述了该方法。