Formal Semantics for the Java Modeling Language

Diplomarbeit

Autor(en):Daniel Bruns
Hochschule:Universität Karlsruhe
Jahr:2009
URL:http://digbib.ubka.uni-karlsruhe.de/volltexte/1000012399

Abstract

This thesis is concerned with the Java Modeling Language (JML), a wide-spread specification language for Java, which is used in both static and runtime analysis of programs. Yet, the official reference mostly lacks semantics, while several tools which implement JML do not agree on their interpretation of JML specifications. Past approaches have all centered around a certain verification tool and are highly depending on specific higher order logics. In this work, we develop a formalization with little requirements. Upon a simple machine model we describe JML artifacts in basic notations such as first order logic. In that, we provide a nearly comprehensive overview of features which cover nearly all specification elements for sequential Java programs.

BibTeX

@MastersThesis{Bruns09,
  author	= {Daniel Bruns},
  title		= {Formal Semantics for the {Java} {Modeling} {Language}},
  year		= 2009,
  month		= jun,
  language	= {english},
  school	= {Universit{\"{a}}t {Karlsruhe}},
  type		= {Diplomarbeit},
  url		= {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000012399},
  urn		= {urn:nbn:de:swb:90-123994},
  license	= {http://creativecommons.org/licenses/by/3.0},
  abstract	= {This thesis is concerned with the Java Modeling Language
		   (JML), a wide-spread specification language for Java, which
		   is used in both static and runtime analysis of programs.
		   Yet, the official reference mostly lacks semantics, while
		   several tools which implement JML do not agree on their
		   interpretation of JML specifications. Past approaches have
		   all centered around a certain verification tool and are
		   highly depending on specific higher order logics. In this
		   work, we develop a formalization with little requirements.
		   Upon a simple machine model we describe JML artifacts in
		   basic notations such as first order logic. In that, we
		   provide a nearly comprehensive overview of features which
		   cover nearly all specification elements for sequential Java
		   programs.}
}