Automatic verification of Dafny programs with traits

Reza Ahmadi, K. Rustan M Leino, Jyrki Nummenmaa

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

    3 Citations (Scopus)

    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.

    Original languageEnglish
    Title of host publicationProceedings for the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015: co-located with ECOOP 2015
    ISBN (Electronic)978-1-4503-3656-7
    DOIs
    Publication statusPublished - 2015
    Publication typeA4 Article in conference proceedings
    Event17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015 -
    Duration: 1 Jan 2015 → …

    Conference

    Conference17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015
    Period1/01/15 → …

    Keywords

    • Boogie
    • Dafny
    • Program verification
    • Traits

    Publication forum classification

    • No publication forum level

    Fingerprint

    Dive into the research topics of 'Automatic verification of Dafny programs with traits'. Together they form a unique fingerprint.

    Cite this