一种利用Dafny构造验证软件的方法
A Tutorial on Using Dafny to Construct Verified Software
摘要：
本文是自动化验证工具领域的新手教程，尽管我们假设读者对Hoare风格的验证相对熟悉。本文除了介绍语言和验证器Dafny的最基本的特点外，还特别强调了如何使用Dafny作为验证程序开发的助手。我们的主要目标是鼓励软件工程社区使用形式化验证工具。
英文摘要：
This paper is a tutorial for newcomers to the field of automated verification tools, though we assume the reader to be relatively familiar with Hoare-style verification. In this paper, besides introducing the most basic features of the language and verifier Dafny, we place special emphasis on how to use Dafny as an assistant in the development of verified programs. Our main aim is to encourage the software engineering community to make the move towards using formal verification tools.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
