Automatic verification of Dafny programs with traits

Reza Ahmadi; K. Rustan M Leino; Jyrki Nummenmaa

doi:10.1145/2786536.2786542

Automatic verification of Dafny programs with traits

Reza Ahmadi, K. Rustan M Leino, Jyrki Nummenmaa

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review

6 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 language	English
Title of host publication	Proceedings for the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015: co-located with ECOOP 2015
Publisher	ACM
ISBN (Electronic)	978-1-4503-3656-7
DOIs	https://doi.org/10.1145/2786536.2786542
Publication status	Published - 2015
Publication type	A4 Article in conference proceedings
Event	17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015 - Duration: 1 Jan 2015 → …

Conference

Conference	17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015
Period	1/01/15 → …

Keywords

Boogie
Dafny
Program verification
Traits

Publication forum classification

No publication forum level

Access to Document

10.1145/2786536.2786542

Cite this

@inproceedings{3e748b744bc54e4e95ec9bd99364d5a6,

title = "Automatic verification of Dafny programs with traits",

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, Boogie, Dafny, Program verification, Traits",

author = "Reza Ahmadi and Leino, {K. Rustan M} and Jyrki Nummenmaa",

year = "2015",

doi = "10.1145/2786536.2786542",

language = "English",

booktitle = "Proceedings for the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015: co-located with ECOOP 2015",

publisher = "ACM",

address = "United States",

note = "17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015 ; Conference date: 01-01-2015",

}

TY - GEN

T1 - Automatic verification of Dafny programs with traits

AU - Ahmadi, Reza

AU - Leino, K. Rustan M

AU - Nummenmaa, Jyrki

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

KW - Boogie

KW - Dafny

KW - Program verification

KW - Traits

KW - Boogie

KW - Dafny

KW - Program verification

KW - Traits

U2 - 10.1145/2786536.2786542

DO - 10.1145/2786536.2786542

M3 - Conference contribution

AN - SCOPUS:84958750086

BT - Proceedings for the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015: co-located with ECOOP 2015

PB - ACM

T2 - 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015

Y2 - 1 January 2015

ER -

Automatic verification of Dafny programs with traits

Abstract

Conference

Keywords

Publication forum classification

Access to Document

Fingerprint

Cite this