dafny

Dafny is a verification-aware programming language

2 years after

Dafny

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, which includes sources, binary downloads for Windows, Mac, GNU/Linux, and FreeBSD, sources, and the issue tracker (old issues are on codeplex).
  • The Rise4fun site, where you can verify Dafny programs in your web browser.

Try Dafny

The easiest way to get started with Dafny is to use rise4fun, where you can write and verify Dafny programs without having install anything. On rise4fun, you will also find the online Dafny tutorial.

Setup

See installation instructions on the wiki and instructions for installing the Dafny mode for Emacs.

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 inpiration 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

Code of Conduct

This project has adopted the Microsoft Open Source Code of Conduct. For more information see the Code of Conduct FAQ or contact [email protected] with any additional questions or comments.

Related Repositories

quine-relay

quine-relay

An uroboros program with 100 programming languages ...

TheVerificationOfDistributedSystem

TheVerificationOfDistributedSystem

Accompanying Repository for The Verification of a Distributed System Talk ...

dafny-sandbox

dafny-sandbox

Dafny for Metatheory of Programming Languages ...

vim-loves-dafny

vim-loves-dafny

a vim plugin for Dafny, a verified programming language. ...

Casper

Casper

A compiler for automatically re-targeting sequential Java code to Apache Spark. ...