Skip to content
/ dafny Public
forked from dafny-lang/dafny

Dafny is a verification-aware programming language

License

Notifications You must be signed in to change notification settings

jaylorch/dafny

 
 

Repository files navigation

Build and Test Gitter

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. 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 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. It is also easy to install Dafny on your own machine in VS Code, which gives you a much better user experience than in the web browser.

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

About

Dafny is a verification-aware programming language

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • C# 56.3%
  • Dafny 35.4%
  • F# 3.1%
  • Java 1.8%
  • Go 0.9%
  • Boogie 0.9%
  • Other 1.6%