@incollection{HuismanAhrendtGrahl2016, author = {Marieke Huisman and Wolfgang Ahrendt and Daniel Grahl and Martin Hentschel}, title = {Formal Specification with the Java Modeling Language}, booktitle = {Deductive Software Verification - The {\KeY} Book: From Theory to Practice}, year = {2016}, publisher = {Springer}, pages = {193--241}, chapter = {7}, part = {II: Specification and Verification}, doi = {10.1007/978-3-319-49812-6_7}, series = {Lecture Notes in Computer Science}, volume = {10001}, month = dec, abstract = {This text is a general, self contained, and tool independent introduction into the Java Modeling Language, JML. It appears in a book about the {\KeY} approach and tool for the verification of Java software, because JML is the dominating starting point of {\KeY} style Java verification. However, this chapter does not depend on any specific tool nor verification methodology in any way. 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.} }
Formal Specification with the Java Modeling Language
Author(s): | Marieke Huisman, Wolfgang Ahrendt, Daniel Grahl, and Martin Hentschel |
---|---|
In: | Deductive Software Verification - The KeY Book: From Theory to Practice |
Publisher: | Springer |
Series: | Lecture Notes in Computer Science |
Volume: | 10001 |
Part: | II: Specification and Verification |
Chapter: | 7 |
Year: | 2016 |
Pages: | 193-241 |
DOI: | 10.1007/978-3-319-49812-6_7 |
Abstract
This text is a general, self contained, and tool independent introduction into the Java Modeling Language, JML. It appears in a book about the KeY approach and tool for the verification of Java software, because JML is the dominating starting point of KeY style Java verification. However, this chapter does not depend on any specific tool nor verification methodology in any way. 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.