Formal Specification with JML

@TechReport{HuismanAhrendtBrunsEtAl14,
  author	= {Marieke Huisman and Wolfgang Ahrendt and Daniel Bruns
		   and Martin Hentschel},
  title		= {Formal Specification with {JML}},
  year		= 2014,
  month		= jul,
  institution	= {Department of Informatics, Karlsruhe Institute of
		   Technology},
  number	= {2014-10},
  series	= {Karlsruhe Reports in Informatics},
  url		= {https://publikationen.bibliothek.kit.edu/1000041881},
  urn		= {urn:nbn:de:swb:90-418817},
  issn		= {2190-4782},
  language	= {english},
  license	= {http://creativecommons.org/licenses/by-nc-nd/3.0/},
  abstract	= {This text is a general, self contained, and tool
		   independent introduction into the \emph{Java Modeling Language}, 
		   JML. It is a preview of a chapter planned to
		   appear in a book about the {\KeY} approach and tool to the
		   verification of Java{} software. JML is the dominating
		   starting point of {\KeY} style Java{} verification. However,
		   this paper does not in any way depend on any tool nor
		   verification methodology. Other chapters in this book talk
		   about the usage of JML in {\KeY} style verification. Here,
		   we only refer to {\KeY} in very few places, without relying
		   on it. This introduction is written for all readers with an
		   interest in formal specification of software in general,
		   and anyone who wants to learn about the JML approach to
		   specification in particular. The authors appreciate any
		   comments or questions that help to improve the text.}
}