KIT | KIT-Bibliothek | Impressum | Datenschutz

Formal Semantics of Model Fields in Annotation-based Specifications

Beckert, Bernhard ORCID iD icon 1; Bruns, Daniel 1
1 Fakultät für Informatik (INFORMATIK), Karlsruher Institut für Technologie (KIT)

Abstract:

It is widely recognized that abstraction and modularization are indispensable for specification of real-world programs. In source-code level program specification and verification, model fields are a common means for those goals. However, it remains a challenge to provide a well-founded formal semantics for the general case in which the abstraction relation defining a model field is non-functional.
In this paper, we discuss and compare several possibilities for defining model field semantics, and we give a complete formal semantics for the general case. Our analysis and the proposed semantics is based on a generalization of Hilbert's epsilon terms.


Volltext §
DOI: 10.5445/IR/1000034594
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2012
Sprache Englisch
Identifikator ISBN: 978-3-642-33346-0
ISSN: 0302-9743
urn:nbn:de:swb:90-345943
KITopen-ID: 1000034594
HGF-Programm 46.12.03 (POF II, LK 01)
Erschienen in KI 2012: advances in artificial intelligence : 35th Annual German Conference on AI, Saarbrücken, Germany, September 24-27, 2012. Ed.: B. Glimm
Verlag Springer-Verlag
Seiten 13-24
Serie Lecture Notes in Computer Science ; 7526
Projektinformation KASTEL I (BMBF, 01BY1172 / 16BY1172)
Nachgewiesen in Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page