结论

我们已经看到了Dafny的主要功能，并将其用于一些有趣的例子，如果是在小方面的话，说明Dafny可以做什么。但是，要真正利用Dafny提供的功能，需要深入学习高级主题:对象、序列和集合、数据结构、引理等。现在您已经熟悉了Dafny的基础知识，您可以在闲暇时阅读关于这些主题的教程。每个教程都被设计成相对独立的主题指南，尽管有些教程可以从事先阅读其他教程中受益。这些例子也是寻找Dafny模型程序的好地方。最后，引用包含了Dafny语法和语义的详细信息，当您只需要知道不相交集合操作符是什么(它是!!)。

tips

即使您不经常使用Dafny，以一种精确的方式准确地写下代码所做的事情，并使用它来证明代码是正确的，这是一种有用的技能。不变量、前置和后置条件以及注释在调试代码中非常有用，也可以作为将来开发人员的文档。当修改或添加代码库时，它们确认现有代码的保证没有被破坏。他们还通过形式化行为和需求并强制执行正确的用法，确保api被正确使用。从不变量推理、考虑前置和后置条件，以及编写断言来检查假设，这些都是通用的计算机科学技能，无论使用哪种语言，这些技能都将使您受益。