Dafny

Dafny
ParadigmImperative, functional
Designed byK. Rustan M. Leino
DeveloperMicrosoft Research, AWS[citation needed]
First appeared2009; 15 years ago (2009)
Stable release
4.9.0 / October 31, 2024; 26 days ago (2024-10-31)
Typing disciplineStatic, strong, safe
LicenseMIT License
Filename extensions.dfy
Websitedafny.org

Dafny is an imperative and functional compiled language that compiles to other programming languages, such as C#, Java, JavaScript, Go and Python. It supports formal specification through preconditions, postconditions, loop invariants, loop variants, termination specifications and read/write framing specifications. The language combines ideas from the functional and imperative paradigms; it includes support for object-oriented programming. Features include generic classes, dynamic allocation, inductive datatypes and a variation of separation logic known as implicit dynamic frames[1] for reasoning about side effects.[2] Dafny was created by Rustan Leino at Microsoft Research after his previous work on developing ESC/Modula-3, ESC/Java, and Spec#.

Dafny is widely used in teaching[citation needed] because it provides a simple, integrated introduction to formal specification and verification; it is regularly featured in software verification competitions (e.g. VSTTE'08,[3] VSCOMP'10,[4] COST'11,[5] and VerifyThis'12[6]).

Dafny was designed as a verification-aware programming language, requiring verification along with code development. It thus fits the "Correct by Construction" software development paradigm. Verification proofs are supported by a mathematical toolbox that includes mathematical integers and reals, bit-vectors, sequences, sets, multisets, infinite sequences and sets, induction, co-induction, and calculational proofs. Verification obligations are discharged automatically, given sufficient specification. Dafny uses some program analysis to infer many specification assertions, reducing the burden on the user of writing specifications. The general proof framework is that of Hoare logic.

Dafny builds on the Boogie intermediate language which uses the Z3 automated theorem prover for discharging proof obligations.[7][8]

  1. ^ Smans, Jan; Jacobs, Bart; Piessens, Frank (2009). Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic (PDF). Proceedings of the Conference on European Conference on Object Oriented Programming. pp. 148–172. doi:10.1007/978-3-642-03013-0_8.
  2. ^ Leino, Rustan (2010). Dafny: An Automatic Program Verifier for Functional Correctness. Proceedings of the Conference on Logic for Programming, Artificial Intelligence, and Reasoning. pp. 348–370. doi:10.1007/978-3-642-17511-4_20.
  3. ^ Leino, Rustan; Monahan, Rosemary (2010). Dafny Meets the Verification Benchmarks Challenge (PDF). International Conference on Verified Software: Theories, Tools, and Experiments. pp. 112–116. doi:10.1007/978-3-642-15057-9_8.
  4. ^ Klebanov, Vladimir; et al. (2011). The 1st Verified Software Competition: Experience Report. Proceedings of the Conference on Formal Methods. pp. 154–168. CiteSeerX 10.1.1.221.6890. doi:10.1007/978-3-642-21437-0_14.
  5. ^ Bormer, Thorsten; et al. (2011). The COST IC0701 Verification Competition 2011. Proceedings of the Conference on Formal Verification of Object-Oriented Software. pp. 3–21. CiteSeerX 10.1.1.396.6170. doi:10.1007/978-3-642-31762-0_2.
  6. ^ Huisman, Marieke; Klebanov, Vladimir; Monahan, Rosemary (2015). "VerifyThis 2012" (PDF). International Journal on Software Tools for Technology Transfer. 17 (6): 647–657. doi:10.1007/s10009-015-0396-8. S2CID 14301377.
  7. ^ "Z3 Homepage". GitHub. 2019-02-07.
  8. ^ de Moura, Leonardo; Bjørner, Nikolaj (2008). Z3: An Efficient SMT Solver. Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis. pp. 337–340. doi:10.1007/978-3-540-78800-3_24.