Formal specification with JML

Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, Martin Hentschel

    Research output: Book/ReportReportProfessional

    40 Downloads (Pure)

    Abstract

    This text is a general, self contained, and tool independent introduction into the Java Modeling Language, JML. It is a preview of a chapter planned to appear in a book about the KeY approach and tool to the verification of Java software. JML is the dominating starting point of KeY style Java verification. However, this paper does not in any way depend on any tool nor verification methodology. Other chapters in this book talk about the usage of JML in KeY style verification. Here, we only refer to KeY in very few places, without relying on it. This introduction is written for all readers with an interest in formal specification of software in general, and anyone who wants to learn about the JML approach to specification in particular. The authors appreciate any comments or questions that help to improve the text.
    Original languageUndefined
    Place of PublicationKarlsruhe
    PublisherDepartment of Informatics, Karlsruhe Institute of Technology
    Number of pages51
    ISBN (Print)2190-4782
    Publication statusPublished - 2014

    Publication series

    NameKarlsruhe Reports in Informatics
    PublisherKarlsruhe Institute of Technology, Department of Informatics
    No.2014-10
    ISSN (Print)2190-4782

    Keywords

    • EC Grant Agreement nr.: FP7/287767
    • METIS-309892
    • EC Grant Agreement nr.: FP7/258405
    • EC Grant Agreement nr.: FP7/2007-2013
    • IR-94636
    • EWI-25720

    Cite this

    Huisman, M., Ahrendt, W., Bruns, D., & Hentschel, M. (2014). Formal specification with JML. (Karlsruhe Reports in Informatics; No. 2014-10). Karlsruhe: Department of Informatics, Karlsruhe Institute of Technology.
    Huisman, Marieke ; Ahrendt, Wolfgang ; Bruns, Daniel ; Hentschel, Martin. / Formal specification with JML. Karlsruhe : Department of Informatics, Karlsruhe Institute of Technology, 2014. 51 p. (Karlsruhe Reports in Informatics; 2014-10).
    @book{56a5e40cbe494172b7692205841a0355,
    title = "Formal specification with JML",
    abstract = "This text is a general, self contained, and tool independent introduction into the Java Modeling Language, JML. It is a preview of a chapter planned to appear in a book about the KeY approach and tool to the verification of Java software. JML is the dominating starting point of KeY style Java verification. However, this paper does not in any way depend on any tool nor verification methodology. Other chapters in this book talk about the usage of JML in KeY style verification. Here, we only refer to KeY in very few places, without relying on it. This introduction is written for all readers with an interest in formal specification of software in general, and anyone who wants to learn about the JML approach to specification in particular. The authors appreciate any comments or questions that help to improve the text.",
    keywords = "EC Grant Agreement nr.: FP7/287767, METIS-309892, EC Grant Agreement nr.: FP7/258405, EC Grant Agreement nr.: FP7/2007-2013, IR-94636, EWI-25720",
    author = "Marieke Huisman and Wolfgang Ahrendt and Daniel Bruns and Martin Hentschel",
    note = "eemcs-eprint-25720",
    year = "2014",
    language = "Undefined",
    isbn = "2190-4782",
    series = "Karlsruhe Reports in Informatics",
    publisher = "Department of Informatics, Karlsruhe Institute of Technology",
    number = "2014-10",

    }

    Huisman, M, Ahrendt, W, Bruns, D & Hentschel, M 2014, Formal specification with JML. Karlsruhe Reports in Informatics, no. 2014-10, Department of Informatics, Karlsruhe Institute of Technology, Karlsruhe.

    Formal specification with JML. / Huisman, Marieke; Ahrendt, Wolfgang; Bruns, Daniel; Hentschel, Martin.

    Karlsruhe : Department of Informatics, Karlsruhe Institute of Technology, 2014. 51 p. (Karlsruhe Reports in Informatics; No. 2014-10).

    Research output: Book/ReportReportProfessional

    TY - BOOK

    T1 - Formal specification with JML

    AU - Huisman, Marieke

    AU - Ahrendt, Wolfgang

    AU - Bruns, Daniel

    AU - Hentschel, Martin

    N1 - eemcs-eprint-25720

    PY - 2014

    Y1 - 2014

    N2 - This text is a general, self contained, and tool independent introduction into the Java Modeling Language, JML. It is a preview of a chapter planned to appear in a book about the KeY approach and tool to the verification of Java software. JML is the dominating starting point of KeY style Java verification. However, this paper does not in any way depend on any tool nor verification methodology. Other chapters in this book talk about the usage of JML in KeY style verification. Here, we only refer to KeY in very few places, without relying on it. This introduction is written for all readers with an interest in formal specification of software in general, and anyone who wants to learn about the JML approach to specification in particular. The authors appreciate any comments or questions that help to improve the text.

    AB - This text is a general, self contained, and tool independent introduction into the Java Modeling Language, JML. It is a preview of a chapter planned to appear in a book about the KeY approach and tool to the verification of Java software. JML is the dominating starting point of KeY style Java verification. However, this paper does not in any way depend on any tool nor verification methodology. Other chapters in this book talk about the usage of JML in KeY style verification. Here, we only refer to KeY in very few places, without relying on it. This introduction is written for all readers with an interest in formal specification of software in general, and anyone who wants to learn about the JML approach to specification in particular. The authors appreciate any comments or questions that help to improve the text.

    KW - EC Grant Agreement nr.: FP7/287767

    KW - METIS-309892

    KW - EC Grant Agreement nr.: FP7/258405

    KW - EC Grant Agreement nr.: FP7/2007-2013

    KW - IR-94636

    KW - EWI-25720

    M3 - Report

    SN - 2190-4782

    T3 - Karlsruhe Reports in Informatics

    BT - Formal specification with JML

    PB - Department of Informatics, Karlsruhe Institute of Technology

    CY - Karlsruhe

    ER -

    Huisman M, Ahrendt W, Bruns D, Hentschel M. Formal specification with JML. Karlsruhe: Department of Informatics, Karlsruhe Institute of Technology, 2014. 51 p. (Karlsruhe Reports in Informatics; 2014-10).