KIT | KIT-Bibliothek | Impressum | Datenschutz

Proving Well-Definedness of JML Specifications with KeY

Kirsten, Michael

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

Open Access Logo


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