Dafny is both a language and a verification tool for creating verified programs. The language has features of object-oriented languages and functional languages. The verification support is based on contract-style verification. This short, easy read seems to be the accompaniment for a tutorial and discusses verification of six different functions that demonstrates contracts and the specification notation, loop invariants, immutable inductive datatypes, mutable datatypes, use of pure functions in specifications, classes, ghost-fields, invariants, and lemmas. Proofs of lemmas are especially interesting because the lemmas are just ghost methods and the body of those methods are the proofs of the lemmas. e.g., to write an inductive proof, one writes a recursive function using a case split to separate the base case from the inductive step.
Developing verified programs with Dafny
K. Rustan M. Leino[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 28 February 2020
2013 35th International Conference on Software Engineering (ICSE)
Volume
Pages 1488-1490
May 2013
Topic(s): tools verification
Note(s): auto-active verification, Boogie verifier, Dafny verifier, ghost code, Z3 solver, SMT solver
Papers: leino:lpair:2010
Volume
Pages 1488-1490
May 2013
Topic(s): tools verification
Note(s): auto-active verification, Boogie verifier, Dafny verifier, ghost code, Z3 solver, SMT solver
Papers: leino:lpair:2010