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 |

Publication

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.