Formal specification with the Java modeling language

Marieke Huisman, Wolfgang Ahrendt, Daniel Grahl, Martin Hentschel

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

    4 Citations (Scopus)
    6 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