Formal specification with the Java modeling language

Marieke Huisman, Wolfgang Ahrendt, Daniel Grahl, Martin Hentschel

  • 1 Citations

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, because JML is the dominating starting point of KeY style Java verification. However, this chapter does not depend on KeY, nor any other specific tool, nor on any specific verification methodology. With this text, the authors aim to provide, for the time being, the definitive, general JML tutorial.
Original languageUndefined
Title of host publicationDeductive Software Verification – The KeY Book
EditorsWolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, Mattoas Ulbrich
Place of PublicationLondon
PublisherSpringer Verlag
Pages193-241
Number of pages49
ISBN (Print)978-3-319-49811-9
DOIs
StatePublished - Dec 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume10001
ISSN (Print)0302-9743

Fingerprint

Modeling languages

Keywords

  • IR-104404
  • EWI-27666

Cite this

Huisman, M., Ahrendt, W., Grahl, D., & Hentschel, M. (2016). Formal specification with the Java modeling language. In W. Ahrendt, B. Beckert, R. Bubel, R. Hähnle, P. H. Schmitt, & M. Ulbrich (Eds.), Deductive Software Verification – The KeY Book (pp. 193-241). (Lecture Notes in Computer Science; Vol. 10001). London: Springer Verlag. DOI: 10.1007/978-3-319-49812-6_7

Huisman, Marieke; Ahrendt, Wolfgang; Grahl, Daniel; Hentschel, Martin / Formal specification with the Java modeling language.

Deductive Software Verification – The KeY Book. ed. / Wolfgang Ahrendt; Bernhard Beckert; Richard Bubel; Reiner Hähnle; Peter H. Schmitt; Mattoas Ulbrich. London : Springer Verlag, 2016. p. 193-241 (Lecture Notes in Computer Science; Vol. 10001).

Research output: ScientificChapter

@inbook{7b991cf1467a45fcaa4172abdb960f38,
title = "Formal specification with the Java modeling language",
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, because JML is the dominating starting point of KeY style Java verification. However, this chapter does not depend on KeY, nor any other specific tool, nor on any specific verification methodology. With this text, the authors aim to provide, for the time being, the definitive, general JML tutorial.",
keywords = "IR-104404, EWI-27666",
author = "Marieke Huisman and Wolfgang Ahrendt and Daniel Grahl and Martin Hentschel",
year = "2016",
month = "12",
doi = "10.1007/978-3-319-49812-6_7",
isbn = "978-3-319-49811-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "193--241",
editor = "Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner Hähnle and Schmitt, {Peter H.} and Mattoas Ulbrich",
booktitle = "Deductive Software Verification – The KeY Book",
address = "Germany",

}

Huisman, M, Ahrendt, W, Grahl, D & Hentschel, M 2016, Formal specification with the Java modeling language. in W Ahrendt, B Beckert, R Bubel, R Hähnle, PH Schmitt & M Ulbrich (eds), Deductive Software Verification – The KeY Book. Lecture Notes in Computer Science, vol. 10001, Springer Verlag, London, pp. 193-241. DOI: 10.1007/978-3-319-49812-6_7

Formal specification with the Java modeling language. / Huisman, Marieke; Ahrendt, Wolfgang; Grahl, Daniel; Hentschel, Martin.

Deductive Software Verification – The KeY Book. ed. / Wolfgang Ahrendt; Bernhard Beckert; Richard Bubel; Reiner Hähnle; Peter H. Schmitt; Mattoas Ulbrich. London : Springer Verlag, 2016. p. 193-241 (Lecture Notes in Computer Science; Vol. 10001).

Research output: ScientificChapter

TY - CHAP

T1 - Formal specification with the Java modeling language

AU - Huisman,Marieke

AU - Ahrendt,Wolfgang

AU - Grahl,Daniel

AU - Hentschel,Martin

PY - 2016/12

Y1 - 2016/12

N2 - 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, because JML is the dominating starting point of KeY style Java verification. However, this chapter does not depend on KeY, nor any other specific tool, nor on any specific verification methodology. With this text, the authors aim to provide, for the time being, the definitive, general JML tutorial.

AB - 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, because JML is the dominating starting point of KeY style Java verification. However, this chapter does not depend on KeY, nor any other specific tool, nor on any specific verification methodology. With this text, the authors aim to provide, for the time being, the definitive, general JML tutorial.

KW - IR-104404

KW - EWI-27666

U2 - 10.1007/978-3-319-49812-6_7

DO - 10.1007/978-3-319-49812-6_7

M3 - Chapter

SN - 978-3-319-49811-9

T3 - Lecture Notes in Computer Science

SP - 193

EP - 241

BT - Deductive Software Verification – The KeY Book

PB - Springer Verlag

ER -

Huisman M, Ahrendt W, Grahl D, Hentschel M. Formal specification with the Java modeling language. In Ahrendt W, Beckert B, Bubel R, Hähnle R, Schmitt PH, Ulbrich M, editors, Deductive Software Verification – The KeY Book. London: Springer Verlag. 2016. p. 193-241. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-49812-6_7