quantifiers - Dafny/Boogie 中的触发器是什么？

Question

我一直在达夫尼一瘸一拐地走着，不了解触发器。也许正因为如此，我写的程序似乎让验证者很为难。有时我会花大量时间摆弄我的证明，试图说服 Dafny/Boogie 它是有效的；当我开始工作时，有时验证速度很慢(这严重降低了我继续工作的能力)。

很难问一个准确的问题，因为我不知道那是什么我不知道。但让我们从基础开始:

什么是触发器？它们什么时候使用？它们是如何推断出来的？一旦我理解了所有这些，接下来我应该阅读什么？

Answer 1

了解触发器绝对是成为 Dafny 专家的重要部分!

我们最近启动了一个frequently asked questions page对于 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) 是一个有效的触发器，因为它提到了所有绑定(bind)变量并且不包含任何解释函数。另一个有效的触发器是表达式 {P(a), R(b)} 的集。一个触发器或另一个(或两者)哪个更好取决于上下文。通常 Dafny 会推断并使用所有有效的、最通用的触发器，因此在这种情况下，它会同时选择 Q(a, b) 和 {P(a), R(b)}。

通常，Dafny 的触发器推理通过查看 e 的所有子表达式来枚举所有有效触发器来工作。然后 Dafny 会过滤掉那些严格意义上不如另一个有效触发器的触发器。 Dafny 选择所有剩余的触发器。

如需额外阅读，我推荐论文 Simplify: A Theorem Prover for Program Checking由 Detlefs、Nelson 和 Saxe 撰写。 Simplify 是一个早期的 SMT 求解器，它开创了启发式使用触发器来处理量词的先河。上述论文的第 5 节详细描述了该方法。