Formal Semantics for the Java Modeling Language

@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		= {https://publikationen.bibliothek.kit.edu/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.}
}