Dafny is a programming language with a program verifier. As you type in your program, the verifier constantly looks over your shoulders and flags any errors. Dafny is currently spread across 3 sites:
- Dafny's homepage, which contains some information about Dafny.
- This site, including
- The Rise4fun site, including a tutorial, where you can verify Dafny programs in your web browser.
Here are some ways to get started with Dafny:
- 4-part course on the Basics of specification and verification of code:
- New overview article: Accessible Software Verification with Dafny, IEEE Software, Nov/Dec 2017
- Online tutorial, focusing mostly on simple imperative programs
- 3-page tutorial notes with examples (ICSE 2013)
- Dafny Quick Reference
- Language reference for the Dafny type system, which also describes available expressions for each type
- Cheatsheet: basic Dafny syntax on two pages
- Dafny Reference Manual [html] [pdf]
- Videos at Verification Corner
The language itself draws pieces of influence from:
- Euclid (from the mindset of a designing a language whose programs are to be verified),
- Eiffel (like the built-in contract features),
- CLU (like its iterators, and inspiration for the out-parameter syntax),
- Java, C#, and Scala (like the classes and traits, and syntax for functions),
- ML (like the module system, and its functions and inductive datatypes), and
- Coq and VeriFast (like the ability to include co-inductive datatypes and being able to write inductive and co-inductive proofs).
- Haskell-to-Dafny translator, by Duncan White
- Vim-loves-Dafny mode for vim, by Michael Lowell Roberts
- Boogie-Friends Emacs mode
Code of Conduct
Dafny itself is licensed under the MIT license. (See LICENSE.txt in the root directory for details.) The subdirectory
third_party contains third party material; see NOTICES.txt for more details.