如何向 Dafny 添加功能？

Question

我想为 Dafny 添加一些基本的便利功能，例如在 Dafny 中定义集合联合的能力（请参阅此问题）。但是 Dafny 的内部结构似乎没有很好的文档记录，我不知道从哪里开始。

如何添加这样的功能？

Answer 1

这是一个很好的问题。我不确定为什么它被否决了。谢谢你的提问。当我开始进入 Dafny 时，我希望我能更好地知道在哪里寻找有关其内部结构的信息。

Rustan 有许多关于如何使用Dafny 的教程/论文/示例。（事实上​​，我会说我们在这里有点为财富的尴尬而苦恼，因为在近十年的时间里，资源如此之多，以至于很难知道从哪里开始。但那是另一天的故事。）另外， Dafny 是一个活生生的项目：事情发生了变化，因此有些文件已经过时了。您应该为此做好准备，并始终愿意打开一个新文件并在现代 Dafny 中尝试一下。

尽管如此，关于Dafny内部的资源相对较少。最好的方法是确保你对 Dafny 背后的理论有透彻的理解，然后阅读代码。（相当不错！）这里有一些具体的提示。

• Dafny 参考手册本质上是对 Dafny 输入语法的注释描述。它最后一次认真编辑是在大约两年前，所以有些东西已经过时了，但它作为 Dafny 功能的一个几乎详尽的列表仍然是无价的。（如果您发现缺少特定内容，请提交 github 问题，我们将尝试修复它们。）我建议您从头到尾阅读。

• 查看 Rustan 的暑期学校课程，该课程对 Dafny 和 Boogie 进行了理论介绍。还可以查看关于 Spec# 的这个早期的暑期学校课程，其中包含许多相同的想法，但速度更加悠闲。

• 学习在 Boogie 中编程。

  • 从（10 年前，但仍然 90% 准确）手册开始这是 Boogie 2。相比之下，深入了解 Boogie 将帮助您了解 Dafny 带来了什么。

  • 请 Dafny 为您翻译一些示例到 Boogie（使用命令行选项/print:foo.bpl），并阅读生成的 Boogie 代码。

  • 阅读Boogie 测试套件以查看更多示例。从textbook目录开始。忽略名称有趣的目录。

  • 另请查看有关 Boogie 比您想象的更复杂的类型系统的这篇论文。（它超越了 Hindley-Milner 多态性！）

• 至少了解一点关于 Z3 的知识。

  • 特别关注它如何使用触发器来处理量词。触发器的 Dafny 级别视图的一个很好的介绍是论文触发器选择策略以稳定自动程序验证器。

  • 请 Boogie 为您翻译一些（小）示例到 Z3（使用命令行选项/proverLog:foo.smt2），并阅读生成的 Z3 代码。这很难，但为了你自己的启迪，值得一两次。它在调试过程中偶尔也会有帮助。

• 深入了解Dafny 测试套件。

  • 阅读测试。测试套件中有很多测试，在许多情况下，这是唯一可以看到某些功能的真实、实时、工作示例的地方。如果测试套件中没有包含某些功能，请提交 Github 问题，我们会尽力处理。

  • 学习运行测试，以便您可以测试您对 Dafny 的改进是否会破坏现有程序。（其基本思路是，以安装的lit测试工具，并在它指向Test的目录。）

• 阅读代码。

  • 总的来说，这是令人耳目一新的好代码。高层结构记录不足，但低层结构通常记录和/或清晰。因此，您的工作是重建高层结构。首先了解 Dafny 的不同阶段——解析、“解析”/类型检查、转换为 Boogie 进行验证、编译为 C# 以执行。
  • 这是main()命令行工具。跟踪并找到阶段并阅读您感兴趣的阶段。

• 问问题。不幸的是，关于 Dafny 的内部结构的具体、详细的问题没有很好的地方。Stack Overflow 不合适；Github 也不是。也许最好的权宜之计是在 Github 上提交“文档请求”问题，我们将看看我们能做些什么。

如果我遗漏了什么，我希望 Rustan 可以插话。

祝你好运，用 Rustan 的话来说：安全编程！

此页面（向下滚动到“Dafny”）还链接到您可能会感兴趣的更多关于 Dafny 的论文。