Formal Semantics of Model Fields in Annotation-based Specifications

@InProceedings{BeckertBruns2012,
  author	= {Bernhard Beckert and Daniel Bruns},
  title		= {Formal Semantics of Model Fields in Annotation-based
		   Specifications},
  year		= 2012,
  month         = sep,
  booktitle	= {{KI 2012}: Advances in Artificial Intelligence},
  editor	= {Birte Glimm and Antonio Kr{\"u}ger},
  publisher	= {Springer-Verlag},
  language	= {english},
  series	= {Lecture Notes in Computer Science},
  volume	= 7526,
  isbn		= {978-3-642-33346-0},
  pages		= {13--24},
  url		= {https://link.springer.com/chapter/10.1007/978-3-642-33347-7_2},
  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 $\varepsilon$ terms.}
}