KIT | KIT-Bibliothek | Impressum | Datenschutz

Proving Well-Definedness of JML Specifications with KeY

Kirsten, Michael ORCID iD icon

Abstract:

Specification methods in formal program verification enable the enhancement of source code with formal annotations as to formally specify the behaviour of a program. This is a popular way in order to subsequently prove software to be
reliable and meet certain requirements, which is crucial for many applications and gains even more importance in modern society. The annotations can be taken as a contract, which then can be verified guaranteeing the specified program element – as a receiver – to fulfil this contract with its caller. However, these functional contracts can be problematic for partial functions, e.g., a division, as certain cases may be undefined, as in this example a division by zero. ... mehr

Abstract (englisch):

Specification methods in formal program verification enable the enhancement of source code with formal annotations as to formally specify the behaviour of a program. This is a popular way in order to subsequently prove software to be reliable and meet certain requirements, which is crucial for many applications and gains even more importance in modern society. The annotations can be taken as a contract, which then can be verified guaranteeing the specified program element – as a receiver – to fulfil this contract with its caller. However, these functional contracts can be problematic for partial functions, e.g., a division, as certain cases may be undefined, as in this example a division by zero. ... mehr


Volltext §
DOI: 10.5445/IR/1000092717
Veröffentlicht am 28.03.2019
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Publikationsjahr 2013
Sprache Englisch
Identifikator urn:nbn:de:swb:90-927170
KITopen-ID: 1000092717
Verlag Karlsruher Institut für Technologie (KIT)
Umfang 77 S.
Art der Arbeit Abschlussarbeit - Bachelor
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page