Formal specification with the Java modeling language

Marieke Huisman, Wolfgang Ahrendt, Daniel Grahl, Martin Hentschel

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

    9 Citations (Scopus)
    25 Downloads (Pure)


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

    Publication series

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


    • IR-104404
    • EWI-27666

    Cite this