Sep 28, 2015
Rustan Leino: Traits and dynamic frames
Dafny is a verification-aware programming language [0]. It includes instantiable classes that can be reasoned about using the _dynamic frames_ specification idiom. Previously, there was no inheritance among classes, but a recent addition to the language added _traits_ [1], which are abstract subperclasses with fields, functions, and methods. In this talk, I describe the traits in Dafny. I then give a tutorial on using dynamic frames and show how these are used with traits. I also mention some future work and bring up some questions I have about the design.
[0] K. Rustan M. Leino. Dafny: An automatic program veri?er for functional correctness. In LPAR-16, volume 6355 of LNAI, pages 348?370. Springer, April 2010.
[1] Reza Ahmadi, K. Rustan M. Leino, Jyrki Nummenmaa. Automatic verification of Dafny programs with traits. FTfJP@ECOOP 2015: 4:1-4:5. July 2015.