Formal Specification with JML
The work
| Title | Formal Specification with JML |
|---|---|
| Authors | Marieke Huisman; Wolfgang Ahrendt; Daniel Bruns; Martin Hentschel |
| Type | technical report |
| Year | 2014 |
| Citekey | huisman2014formal |
Where it appeared
| Publisher | Karlsruhe Institute of Technology |
|---|---|
| Series | Karlsruhe Reports in Informatics |
| Number in series | 2014,10 |
Identifiers
| DOI | 10.5445/ir/1000041881 |
|---|---|
| OpenAlex | W2149931491 |
Access
| Landing page | https://publikationen.bibliothek.kit.edu/1000041881 |
|---|---|
| Free full text | https://research.utwente.nl/en/publications/formal-specification-with-jml(56a5e40c-be49-4172-b769-2205841a0355).html |
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.
Copy held
| Kind | PDF, 405.0 kB |
|---|---|
| Retrieved | 2026-08-09 |
| Held | local, for personal reference |
| Where it came from | https://publikationen.bibliothek.kit.edu/1000041881/3143677 |
Where this came from
| How it got here | the agent went looking · found via openalex |
|---|---|
| First seen | 2026-08-04 |
| Record | reviewed by a person |
| Approved | 2026-08-21 |
Cite it as
@techreport{huisman2014formal,
title = {Formal Specification with JML},
author = {Marieke Huisman and Wolfgang Ahrendt and Daniel Bruns and Martin Hentschel},
year = {2014},
publisher = {Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
volume = {2014,10},
doi = {10.5445/ir/1000041881},
url = {https://research.utwente.nl/en/publications/formal-specification-with-jml(56a5e40c-be49-4172-b769-2205841a0355).html},
}
This record lives at https://refs.drheap.org/huisman2014formal/ and will keep doing so.