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

#### Begutachtete Veröffentlichung in Tagungsband

Autor(en):Bernhard Beckert und Daniel Bruns
In:10th KeY Symposium
Jahr:2011
URL:http://digbib.ubka.uni-karlsruhe.de/volltexte/1000024829

## 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 ε terms.

## Anmerkung

Extended Abstract

## BibTeX

@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},
language	= {english},
month		= aug,
url		= {http://digbib.ubka.uni-karlsruhe.de/volltexte/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.}
}