代码之家 › 专栏 › 技术社区 › Jason Orendorff Oliver

Dafny/Boogie的触发器是什么?

boogie dafny quantifiers

1

Jason Orendorff Oliver · 技术社区 · 7 年前

我在达夫尼一直一瘸一拐地走着,不明白触发点。可能结果是,我编写的程序似乎给验证器带来了困难。有时我花大量时间修改我的证明,试图说服dafny/boogie它是有效的;当我得到一些有用的东西时,有时验证起来很慢(这严重降低了我继续工作的能力)。

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

什么是触发器?什么时候用?如何推断? 一旦我明白了这些, 接下来我应该读什么?

1 回复 | 直到 7 年前

1

James Wilcox 7 年前

了解触发因素绝对是成为达夫尼专家的重要组成部分!

我们最近开始 frequently asked questions page 对于dafny,它包含了对触发器的相当广泛的描述。我建议你从阅读FAQ的那一部分开始。(此答案的其余部分假设您已经这样做了。)

有一件事没有涉及,那就是如何推断触发器。(我很快会将这个答案的编辑版本添加到常见问题解答中。)触发器实际上可能在两个不同的级别被推断出来: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将推断并使用所有有效的、最大限度通用的触发器,因此在本例中,它将同时选择 问题(a,b) 和 {p(a),r(b)} 。

一般来说,dafny的触发器推断是通过查看 e . 然后dafny过滤掉比另一个有效触发器更不通用的触发器。dafny选择所有剩余的触发器。

为了进一步阅读,我推荐这篇论文 Simplify: A Theorem Prover for Program Checking 德特勒夫斯,尼尔森和萨克斯。simplify是一个早期的smt求解器,它开创了启发式使用触发器处理量词的先河。本文第5节对该方法进行了详细的技术描述。