Dafny：支持验证的编程语言

Dafny是一种带有程序验证器的编程语言。当您键入程序时，验证器会不断检查您的肩膀并标记任何错误。此GitHub站点包含以下材料：

有关Dafny语言和工具的文档位于此处。在线和pdf版都有参考手册。(如果需要，可以生产乳胶版本。)。

您可以在Stack Overflow上询问有关Dafny的问题，也可以在Dafny上参与一般性讨论。

开始使用Dafny最简单的方法是使用rise4ful，在那里您可以编写和验证Dafny程序，而无需安装任何东西。在rise4ful上，您还可以找到Dafny在线教程。在您自己的机器上使用VS Code安装Dafny也很容易，这比在Web浏览器中给您提供了更好的用户体验。

Dafny类型系统的语言参考，它还描述了每种类型的可用表达式。

欧几里德(从设计其程序要被验证的语言的思维模式)，

CoQ和VeriFast(比如包含协同归纳数据类型的能力，以及能够编写归纳和协同归纳证明的能力)。

为了强制执行一些基本的样式约定，我们采用了预提交。我们重用了它们的默认钩子。当您克隆Dafny时，请按照说明安装Pre-Commit。例如，在OSX上。

该项目采用了Microsoft开放源代码行为准则。有关更多信息，请参阅行为准则常见问题或联系[email protected]提出任何其他问题或意见。

达夫尼本身是根据麻省理工学院的许可证获得许可的。(有关详细信息，请参阅根目录中的LICENSE.txt。)。子目录Third_party包含第三方材料；有关详细信息，请参阅NOTICES.txt。