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

@InProceedings{BeckertBruns11,
  author	= {Bernhard Beckert and Daniel Bruns},
  title		= {Formal Semantics of Model Fields Inspired by a
		   Generalization of {Hilbert's} $\varepsilon$ Terms},
  note		= {Extended Abstract},
  year		= 2011,
  booktitle	= {10th {\KeY} Symposium},
  editor	= {Ahrendt, Wolfgang and Bubel, Richard},
  address	= {Nijmegen, the Netherlands},
  language	= {english},
  month		= aug,
  url		= {https://publikationen.bibliothek.kit.edu/1000024829},
  urn		= {urn:nbn:de:swb:90-248290},
  abstract	= {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 $\varepsilon$
		   terms.}
}