Dafny with traits: verifying object oriented programs
Ahmadi, Reza (2014)
Ahmadi, Reza
2014
MDP in Software Development
Informaatiotieteiden yksikkö - School of Information Sciences
This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.
Hyväksymispäivämäärä
2014-11-17
Julkaisun pysyvä osoite on
https://urn.fi/URN:NBN:fi:uta-201411192332
https://urn.fi/URN:NBN:fi:uta-201411192332
Tiivistelmä
Dafny is a programming language supporting verified high level programming. It has many features that a modern programming language has, like classes, generic classes, functions, and, methods. However, some aspects of object oriented programming do not exist in Dafny. For instance, it is not possible to write programs with classes and subclasses and then verify the subclasses. In order to enrich the language with the mentioned feature, this thesis introduces traits to Dafny. A trait in Dafny may introduce states, methods and functions with or without bodies. A class, then, inherits from a trait and may override the body-less methods and functions. There are also specifications for methods and functions in a trait that specify the intention of a particular method or function. In terms of the specifications, the class must provide the specifications, for annotating the functions and methods, possibly stronger. This has the drawback of repeating the specifications but it also increases readability as one can look at the class and immediately figure out what specifications govern the behavior of a method or a function.
The new feature, traits, provides polymorphism, information hiding, and reusability. Dynamic dispatch is now also available with the help of the introduced traits.
The new feature, traits, provides polymorphism, information hiding, and reusability. Dynamic dispatch is now also available with the help of the introduced traits.