celdir/dafny

Dafny is a verification-aware programming language

Our Work

Creating a Threading Library

We will extend the Dafny programming language by adding multithreading support with the following features/functionality:

• Creating new threads and accessing handles to those threads
• Sending messages to other threads by their handles
• Concept of simultaneous code in proof engine
• Language support for synchronized functionality that ensures appropriate facts about simultaneous access
• Shared variables with requirements about simultaneous access
• Mutex lock library with appropriate simultaneous-code-related propositions required and ensured

Path Compression (Simple Substitutions)

Using Dafny's sophisticated proof construction, a significant amount of metadata relating to nontrivial facts about the functionality of compiled Dafny code is available. Using this data, optimizations can be made to the code that would have otherwise been unavailable to the compiler. One such example is simple path compression: By analyzing the inputs, outputs, requirements, ensures and side-effects of different subroutines, some routines can be found to have more efficient versions with the same effect.

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:

• 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
• For more papers on Dafny, see the Dafny section of Rustan Leino's paper page

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

• Haskell-to-Dafny translator, by Duncan White
• Vim-loves-Dafny mode for vim, by Michael Lowell Roberts
• Boogie-Friends Emacs mode

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.

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.