TUTCRIS - Tampereen teknillinen yliopisto

TUTCRIS

Automatic verification of Dafny programs with traits

Tutkimustuotosvertaisarvioitu

Yksityiskohdat

AlkuperäiskieliEnglanti
OtsikkoProceedings for the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015: co-located with ECOOP 2015
KustantajaAssociation for Computing Machinery, Inc
ISBN (elektroninen)9781450336567
DOI - pysyväislinkit
TilaJulkaistu - 7 heinäkuuta 2015
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisussa
Tapahtuma17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015 - Prague, Tshekki
Kesto: 7 heinäkuuta 2015 → …

Conference

Conference17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015
MaaTshekki
KaupunkiPrague
Ajanjakso7/07/15 → …

Tiivistelmä

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.