Dafny: Statically Verifying Functional Correctness

TL;DR

Dafny is a language and verifier that enables automatic static verification of functional correctness through features like pre/postconditions, invariants, and mathematical proofs.

Contribution

This paper introduces Dafny, a new language and verifier that integrates programming with formal specification and automated proof techniques.

Findings

Dafny effectively verifies functional correctness of programs.

The language supports various specification constructs like invariants and quantifiers.

Dafny translates code into mathematical proofs for verification.

Abstract

This report presents the Dafny language and verifier, with a focus on describing the main features of the language, including pre- and postconditions, assertions, loop invariants, termination metrics, quantifiers, predicates and frames. Examples of Dafny code are provided to illustrate the use of each feature, and an overview of how Dafny translates programming code into a mathematical proof of functional verification is presented. The report also includes references to useful resources on Dafny, with mentions of related works in the domain of specification languages.