# Formal Specification with JML

#### Technical Report

Author(s):Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel
Institution:Department of Informatics, Karlsruhe Institute of Technology
Series:Karlsruhe Reports in Informatics
Number:2014-10
Year:2014
URL:http://digbib.ubka.uni-karlsruhe.de/volltexte/1000041881

## Abstract

This text is a general, self contained, and tool independent introduction into the 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.

## BibTeX

@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		= {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000041881},
urn		= {urn:nbn:de:swb:90-418817},
issn		= {2190-4782},
language	= {english},
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.}
}