Formal specification with the Java modeling language

Marieke Huisman, Wolfgang Ahrendt, Daniel Grahl, Martin Hentschel

Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

3 Citations (Scopus)
3 Downloads (Pure)

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
Pages193-241
Number of pages49
ISBN (Print)978-3-319-49811-9
DOIs
Publication statusPublished - Dec 2016

Publication series

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

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. https://doi.org/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. editor / Wolfgang Ahrendt ; Bernhard Beckert ; Richard Bubel ; Reiner Hähnle ; Peter H. Schmitt ; Mattoas Ulbrich. London : Springer, 2016. pp. 193-241 (Lecture Notes in Computer Science).
@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",
language = "Undefined",
isbn = "978-3-319-49811-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "193--241",
editor = "Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"a}hnle and Schmitt, {Peter H.} and Mattoas Ulbrich",
booktitle = "Deductive Software Verification – The KeY Book",

}

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, London, pp. 193-241. https://doi.org/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, 2016. p. 193-241 (Lecture Notes in Computer Science; Vol. 10001).

Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

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

A2 - Ahrendt, Wolfgang

A2 - Beckert, Bernhard

A2 - Bubel, Richard

A2 - Hähnle, Reiner

A2 - Schmitt, Peter H.

A2 - Ulbrich, Mattoas

PB - Springer

CY - London

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. 2016. p. 193-241. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-49812-6_7