Available under an MIT License, Dafny is a verification-ready programming language that can compile to C#, Go, Java, or JavaScript.
Designed by K. Rustan M. Leino, and originally developed by Microsoft in 2009, Dafny makes it easy to write correct code.
The language relies on high-level annotations to reason about and prove the correctness of the code, so that there are no runtime errors and the compiled code does what the programmer wants it to do. The effect of a piece of code can be given abstractly through the use of a natural, high-level expression of the desired behavior, which is easy and reliable. Dafny then generates proof that the code matches the annotations, if they are correct.
Dafny is an imperative and functional compiled language that supports formal specifications through preconditions, postconditions, loop invariants, and loop variants. Combining concepts from the functional and. imperative paradigms, the language included limited support for object-oriented programming.
Used widely in teaching, Dafny builds on the Boogie intermediate language, which uses the Z3 automated theorem prover for discharging proof obligations.
The Dafny programming language is the focal point of this portion of our guide. Online resources dedicated to the programming language are appropriate topics for this category, as are any IDEs or other tools designed to facilitate Dafny programming, along with Dafny user groups, forums, tutorials, or guides.
Recommended Resources
Powered by Boogie and Z3, Dafny can be run from the command line on Windows or other platforms, although the preferred way is to run it in Microsoft Visual Studio, where its verifier runs in the background while the programmer is editing the program. The official program language site provides an overview of the language, including its programming concepts and methods, as well as information about its toolbox for mathematical proofs. Download links and links to other resources are provided.
https://dafny.org/
Hosted on the University of Waterloo site, this is a guide to getting started with Dafny, including an introduction to the language, methods, preconditions, postconditions, assertions, functions, loop invariants, termination, arrays, quantifiers, predicates, framing, binary search, tutorials, and conclusions relating to the major features of the language, examples of what it can do, and the ways in which it can be used. The tutorials include several aspects of programming with Dafny.
https://ece.uwaterloo.ca/~agurfink/stqam/rise4fun-Dafny/
Dafny: A Language and Program Verifier for Functional Correctness
Maintained at Microsoft Research, an overview of the programming language is provided, along with links to where it can be downloaded, and where the source code can be obtained. Data on benchmarks and competitions, quick references, and a list of universities that are (or have) using Dafny in some capacity in lectures and class work. Links to other online resources on the language are also provided with profiles of people involved, and publications and videos relating to Dafny.
https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/
Designed by K. Rustan M. Leino while he was at Microsoft Research, the Dafny programming language is available under the MIT License, and it is currently under continuous development at GitHub, which includes the source code and repositories, which details about each, including license data, libraries, and request-for-feature discussions. Projects and packages related to the language are available, and profiles of people involved in its continued development are included.
https://github.com/dafny-lang/
The primary designer of the Dafny programming language, K. Russian M. Leino is a Senior Principal Applied Scientist in the Automated Reasoning Group at Amazon Web Services. Prior to his employment with Amazon, he was Principal Researcher at Microsoft Research. An introduction, CV, papers, projects, and other activities and accomplishments are discussed, and a series of notes with tips on advanced features, explanations, and comparisons of related constructs in the Dafny language are included.
http://leino.science/
