Tampere University of Technology

TUTCRIS Research Portal

Automatic verification of Dafny programs with traits

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

Details

Original languageEnglish
Title of host publicationProceedings for the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015: co-located with ECOOP 2015
PublisherAssociation for Computing Machinery, Inc
ISBN (Electronic)9781450336567
DOIs
Publication statusPublished - 7 Jul 2015
Publication typeA4 Article in a conference publication
Event17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015 - Prague, Czech Republic
Duration: 7 Jul 2015 → …

Conference

Conference17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015
CountryCzech Republic
CityPrague
Period7/07/15 → …

Abstract

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.

Keywords

  • Boogie, Dafny, Program verification, Traits