Dafny Power User

Dafny Power User is a series of notes with tips about advanced features, explanations and comparisons of related constructs, and general thoughts about the Dafny language. Each note assumes that you have some basic familiarity with Dafny. The notes can be read in any order.

• Calling Lemmas Automatically
• Statement versus Expression Syntax
• Comprehensions
• Short-Circuit Operators
• Automatic Induction
• Type-Parameter Completion
• old and unchanged
• Functions over Set Elements
• Iterating over a Collection
• Different Styles of Proofs
• Case study of definitions, proofs, algorithm correctness: GCD
• Type-parameter modes: variance and cardinality preservation
• The Parent Trick for proving termination, and a function-by-method use case
• Working with coinduction, extreme predicates, and ordinals
• How to choose your number types

Here are some publications that give information, tutorials, or advanced coverage of some Dafny features:

• Modular Verification Scopes via Export Sets and Translucent Exports
  (K. Rustan M. Leino and Daniel Matichuk; ARND 2018, © Springer)
  This paper describes the module system, export sets, and imports.

• Verified Calculations
  (K. Rustan M. Leino and Nadia Polikarpova; VSTTE 2013, © Springer)
  This paper introduces the calc statement, which is the primary construct for writing your own proofs in Dafny.

• Modeling Concurrency in Dafny
  (K. Rustan M. Leino; SETSS 2017, © Springer)
  Dafny does not support concurrency, but you can model the execution of concurrent programs and protocols. As this tutorial paper describes, this modeling is done in a style akin to that of TLA+, UNITY, Event-B, or action systems.

• Using Dafny, an Automatic Program Verifier
  (Luke Herbert, K. Rustan M. Leino, and Jose Quaresma; LASER 2011, © Springer)
  If you’re working with mutable, dynamically allocated storage in Dafny, you need to know about abstraction and dynamic frames. One account of these is given in sections 8 and 9 of this tutorial.

• Automating Theorem Proving with SMT
  (K. Rustan M. Leino; ITP 2013, © Springer)
  When you specify and verify more difficult programs in Dafny, you need functions and proofs. This is also true if you want to use Dafny as an interactive proof assistant to write formal models and prove theorems. This paper contains some simple examples of functions, induction, and (advanced!) co-induction. (Note, in current Dafny syntax, ghost method is called lemma and comethod is called colemma.)

• Automatic verification of Dafny programs with traits
  (Reza Ahmadi, K. Rustan M. Leino, and Jyrki Nummenmaa; FTfJP 2015, © ACM)
  Traits are abstract superclasses, variations of which go by various names like interfaces or mix-ins. This paper describes simple traits in Dafny. Since this paper was written, traits have been expanded and traits can now take type parameters and extend other traits.

• Well-founded Functions and Extreme Predicates in Dafny: A Tutorial
  (K. Rustan M. Leino; IWIL-2015, © EPiC)
  Describes Dafny’s inductive predicate and copredicate declarations, along with inductive lemma and colemma. These are advanced features and not just simply a recursive predicate or lemma. Note, the publication talks about a restriction to continuous functors. Since the publication, this restriction has been removed in Dafny. This is achieved by changing the type of the index k in the paper (see its equations (11) and (12)) from nat to ORDINAL. If you really want the previous nat, Dafny offers some syntax for doing so for each (co-)inductive predicate (see the Dafny test suite for examples).

• Programming Language Features for Refinement
  (Jason Koenig and K. Rustan M. Leino; REFINE 2015, © EPTCS)
  This paper describes Dafny’s refinement modules. These are advanced features aimed at letting you write programs in stages, where each stage introduces more details. However, as the paper reports, these features are not as easy to use as one would like. So, if you’re just looking for a way to separate a module’s implementation from its interface, then it is instead the paper “Modular Verification Scopes via Export Sets and Translucent Exports” above that you want to read.

• Compiling Hilbert’s epsilon operator
  (K. Rustan M. Leino; LPAR-20, © EPiC)
  This paper goes through design considerations of the :| (“assign such that” or “let such that”) operator in Dafny. For a more direct example, see the Dafny Power User note Functions over a set above.