Formal Semantics for the Java Modeling Language

@InProceedings{Bruns10,
  author	= {Daniel Bruns},
  title		= {Formal Semantics for the {Java} {Modeling} {Language}},
  note		= {Best Paper Award},
  year		= 2010,
  month		= mar,
  booktitle	= {Informatiktage 2010},
  address	= {Bonn, Germany},
  pages		= {15--18},
  publisher	= {Gesellschaft f{\"u}r Informatik},
  series	= {Lecture Notes in Informatics},
  volume	= {S-9},
  isbn		= {978-3-88579-443-1},
  url		= {http://subs.emis.de/LNI/Seminar/Seminar09/S-09.pdf},
  language	= {english},
  abstract	= {A common critique of formal methods in software
		   development practise is, that they are not readily
		   understandable and thus not widely used. The Java Modeling
		   Language (JML) was created in an attempt to bridge that
		   gap. By building upon the syntax of Java it is meant to be
		   easily accessible to the common user -- who might not be
		   skilled in formal modeling. Due to this advantage, JML has
		   quickly become one of most popular specification languages
		   to use with both static and runtime analysis of programs.
		   JML specifications are written in a Java-like expression
		   language as comments straight into source files. It
		   provides both in-code assertions as well as method
		   contracts and class invariants which are indicated by
		   appropriate preceding keywords. However, the official
		   reference mostly lacks a clear definition of semantics. In
		   turn, several tools implementing JML syntax use their own
		   interpretations. Past approaches to formal semantics have
		   rather been documentations of those tools than providing a
		   unified reference.}
}