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.

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

  • Well-founded Functions and Extreme Predicates in Dafny: A Tutorial

    • 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).
  • Modular Verification Scopes via Export Sets and Translucent Exports

    • This paper describes the module system, export sets, and imports. (© Springer)
  • Modeling Concurrency in Dafny

    • 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. (© Springer)
  • Using Dafny, an Automatic Program Verifier

    • 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. (© Springer)

©2019 K.R.M. Leino - Split Template by One Page Love