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 ε terms. © 2012 Springer-Verlag.
CITATION STYLE
Beckert, B., & Bruns, D. (2012). Formal semantics of model fields in annotation-based specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7526 LNAI, pp. 13–24). https://doi.org/10.1007/978-3-642-33347-7_2
Mendeley helps you to discover research relevant for your work.