达夫尼的详尽战术清单?

Exhaustive List of Tactics In Dafny?

我是新来的达芙妮,正在验证。我了解到,当dafny prover验证程序失败时,用户必须为验证程序使用guidance/hints注释该程序。但是,我无法预料 dafny 验证器何时何地会失败。而像 Coq 这样的东西提供了一个详尽的策略列表,可以在证明中使用。

例如:在这个 example (Section 4) 中,通过简单地查看引理“对于所有 n >= 1,f(n) = 2^{3n} - 3^{ n} 可以被 5 整除。”及其证明,我无法预料 dafny 验证者何时何地需要提示。

是否有有关 dafny 需要 hints/guidance 的场景的指南?

作为一个相对有经验的 Dafny 用户来说,我不会说我总是能够完美地预测 Dafny 何时需要帮助。我只是让验证者告诉我。

由于需要验证者的频繁反馈,因此您使用可以在后台为您 运行 验证者并给您漂亮的红色波浪线的编辑器(vscode 和 emacs 都有开箱即用的扩展。

至于详尽的战术清单,我听说你来自哪里,但这样的清单对于 Dafny 来说并不存在。底层求解器要么得到它,要么不得到它,并且有一种艺术可以弄清楚什么样的事情对它有帮助或没有帮助。与 Coq 等交互式工具不同,您无法直接“查看”问题所在。

如何“看到”你看不到的东西

也就是说,您可以学习如何通过使用类似二进制搜索的简单技术有效地调试验证问题。例如,如果 ensures 子句失败,我可能会将其复制粘贴为方法底部的断言。然后,如果该断言由 && 组合在一起的两件事组成,我可能会分别断言它们中的每一个。然后,如果其中一个连词使用谓词定义,我可能会手动复制粘贴并内联该谓词,并进行进一步的手动简化,以缩小失败的部分。

既然您已经将问题缩小到单个 line/definition,并且无法进一步手动扩展或简化,您需要一个注释。

您可以添加哪些类型的注释

在我的脑海中,我会区分两种在实践中很重要的“帮助”验证者。

  • 接口注释,其中包括pre/postconditions、修改子句、和循环不变量。这些注释会影响 Dafny 要求底层求解器证明的逻辑公式。通过调整这些注释,您可以将无法证明的公式变成可证明的公式。
  • 局部注释,通常以断言语句的形式出现。 Dafny 可以推理的很多有趣的事情都涉及量词 (forall/exists)。即使您的程序没有显式使用任何量词,它们也潜伏在 Dafny 的基本数据结构(例如序列、集合和映射)的内部。不幸的是,关于量词的推理通常是不可判定的,这意味着底层求解器基于在很多时候都有效但并非始终有效的启发式方法。在这些情况下,通过断言语句提及其他真实事实可以“触发”求解器进行不同的推理,从而证明公式。

这两个注解的区别在于接口注解改变了验证问题的逻辑内容,而本地注解保持基本验证问题不变,只是提到了一些额外的有用事实。

结论

Dafny 的学习曲线有点奇怪。一开始一切都很好,感觉非常自然和美妙。然后在某个时候,您开始 运行 遇到对您来说毫无意义的验证错误。您的第一反应是随机地戳一下代码,直到这些错误消失。随着时间的推移,您会更好地了解哪些事情对 Dafny 有帮助,哪些没有帮助。

学习(或教授!)这些策略很难。如果可以,我建议您找一位在与 Dafny 一起工作时可以经常交谈的专家。在没有本地专家的情况下,您可以继续在这里发帖,或者您可以尝试gitter chat。 (我自己不是 gitter 的忠实粉丝,但社区中的其他人使用它。)

最后,我建议阅读 Dafny 上的(很可能是压倒性的)参考资料 material。我建议从 FAQ and the tutorial. Then you can take a look at the Dafny power user and the reference manual. You might also find this Systems Software Verification Summer Camp 2020 开始有用。它教授二进制搜索技术(但仅作为旁注——总共有大约 15 小时的视频讲座,主要是关于验证分布式系统的模型)。