Formal Specification with the Java Modeling Language

Buchkapitel

Autor(en):Marieke Huisman, Wolfgang Ahrendt, Daniel Grahl und Martin Hentschel
In:Deductive Software Verification - The KeY Book: From Theory to Practice
Verleger:Springer
Reihe:Lecture Notes in Computer Science
Band:10001
Kapitel:7
Jahr:2016
Seiten: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.

BibTeX

@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},
  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.}
}