KIT | KIT-Bibliothek | Impressum | Datenschutz

Formal Semantics of Model Fields Inspired by a Generalization of Hilbert's e Terms

Beckert, Bernhard ORCID iD icon; Bruns, Daniel

It is widely recognized that abstraction and modularization are indispensable for specification of real-world programs. In source-code level program specification languages, such as the Java Modeling Language (JML), model fields are a common means for achieving abstraction and information hiding. However, there is yet no well-defined formal semantics for the general case in which the abstraction relation defining a model field is non-functional and may contain references to other model fields. In this contribution, 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 inspired by a generalization of Hilbert's ε terms.

Volltext §
DOI: 10.5445/IR/1000024829
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2011
Sprache Englisch
Identifikator urn:nbn:de:swb:90-248290
KITopen-ID: 1000024829
Erschienen in Proceedings of the 10th KeY Symposium, August 26-27. Hrsg.: W. Ahrendt
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page