KIT | KIT-Bibliothek | Impressum
Open Access Logo
§
Volltext
URN: urn:nbn:de:swb:90-345943

Formal Semantics of Model Fields in Annotation-based Specifications

Beckert, Bernhard; Bruns, Daniel

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.


Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Jahr 2012
Sprache Englisch
Identifikator ISBN: 978-3-642-33346-0
ISSN: 0302-9743
KITopen ID: 1000034594
HGF-Programm 46.12.03; 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, Berlin
Seiten 13-24
Serie Lecture Notes in Computer Science ; 7526
Projektinformation KASTEL I (BMBF, 01BY1172)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page