介绍

Dafny是一种旨在简化编写正确代码的语言。这意味着不存在任何运行时的错误，同时在实际做程序员希望它做的事情上也是正确的。为了实现这一点，Dafny依赖于高级注释来推理和证明代码的正确性。一段代码的效果可以抽象地给出，使用期望行为的自然、高级表达式，这更容易编写，也更不容易出错。Dafny然后生成代码与注释匹配的证明(当然，假设它们是正确的!)。Dafny将编写无bug的代码的负担变成了编写无bug的注释。这通常比编写代码更容易，因为注释更短、更直接。例如，Dafny中下面的注释片段表示数组中的每个元素都是严格正的:

forall k: int :: 0 <= k < a.Length ==> 0 < a[k]

这意味着对于数组中所有的索引为k的整数，索引处的值大于0。通过编写这些注释，可以确信代码是正确的。此外，编写注释的行为可以帮助人们在更深的层次上理解代码正在做什么。 除了证明与用户提供的注释的对应关系外，Dafny还证明没有运行时错误，比如索引越界、空解引用、除零等。这是一个强有力的保证，是使用Dafny和类似工具的一个强有力的例子。Dafny也证明了代码的终止，除了在特殊指定的循环中。 让我们开始编写一些Dafny程序。