Dafny：静态验证函数正确性

本报告介绍了Dafny语言和验证器，重点描述了该语言的主要特性，包括前置条件和后置条件、断言、循环不变量、终止度量、量词、谓词和框架。提供了Dafny代码示例以说明每个特性的使用，并概述了Dafny如何将编程代码转换为函数验证的数学证明。报告还包含了Dafny相关有用资源的引用，并提及了规约语言领域的相关工作。