/dafny

Dafny is a verification-aware programming language

Primary LanguageC#OtherNOASSERTION

Build and Test Gitter

Dafny is a verification-ready programming language. As you type in your program, Dafny's verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you're done, Dafny can compile your code to C#, Java, JavaScript or Go (more to come!), so it can integrate with your existing workflow.

vs-code-dafny-2 0 0-demo

Dafny will give you assurance that your code meets the specifications you write, while letting you write both code and specifications in the Dafny programming language itself. Since verification is an integral part of development, it will thus reduce the risk of costly late-stage bugs that are typically missed by testing.

Dafny has support for common programming concepts such as classes and trait inheritance, inductive datatypes that can have methods and are suitable for pattern matching, lazily unbounded datatypes, subset types e.g. for bounded integers, lambdas, and immutable and mutable data structures.

Dafny also offers an extensive toolbox for mathematical proofs, such as unbounded and bounded quantifiers, calculational proofs, pre- and post-conditions, termination conditions, loop invariants, and read/write specifications.

Dafny

This github site contains these materials:

Documentation about the dafny language and tools is located here. A reference manual is available both online and as pdf. (A LaTeX version can be produced if needed.)

Community

You can ask questions about Dafny on Stack Overflow or participate in general discussion on Dafny's Gitter.

Try Dafny

The easiest way to try out Dafny is to install Dafny on your own machine in Visual Studio Code and follow along with the Dafny tutorial. You can also download and install the Dafny CLI if you prefer to work from the command line.

Read more

Here are some ways to get started with Dafny:

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).

External contributions

Contributors

To enforce some basic style conventions, we've adopted pre-commit. We're using their default hooks. When you clone Dafny, install pre-commit as per the instructions. For example, on macOS you do

$ brew install pre-commit

Then run

$ pre-commit install

This will install pre-commit hooks in your .git/hooks directory.

License

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.