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:

  • Modular Verification Scopes via Export Sets and Translucent Exports

    • This paper describes the module system, export sets, and imports. (© Springer)
  • Verified Calculations

    • This paper introduces the calc statement, which is the primary construct for writing your own proofs in Dafny. (© 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)
  • 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).
  • Programming Language Features for Refinement

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

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