Automatic Verification of Dafny Programs with Traits
- Reza Ahmadi ,
- Rustan Leino ,
- Jyrki Nummenmaa
FTfJP '15 Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, Prague, Czech Republic |
This paper describes the design of traits, abstract superclasses, in the verification-aware programming language Dafny. Although there is no inheritance among classes in Dafny, the traits make it possible to describe behavior common to several classes and to write code that abstracts over the particular classes involved. The design incorporates behavioral specifications for a trait’s methods and functions, just like for classes in Dafny. The design has been implemented in the Dafny tool.
Publication Downloads
Dafny
January 2, 2017
Dafny is a verification-aware programming language.