Formal specification with the Java modeling language

Marieke Huisman, Wolfgang Ahrendt, Daniel Grahl, Martin Hentschel

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

    5 Citations (Scopus)
    11 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