Formal Semantics of Model Fields in Annotation-based Specifications

Reviewed Paper In Proceedings

Author(s):Bernhard Beckert and Daniel Bruns
In:KI 2012: Advances in Artificial Intelligence
Publisher:Springer-Verlag
Series:Lecture Notes in Computer Science
Volume:7526
Year:2012
Pages:13-24
URL:http://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 ε terms.

BibTeX

@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		= {http://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.}
}