Formal Semantics of Model Fields in Annotation-based Specifications
Bernhard Beckert and Daniel Bruns
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.