# 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

## 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},
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.}
}