Extending JML Specifications with Temporal Logic

Kerry Trentelman, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

33 Citations (Scopus)


This paper proposes an extension of the Java Modeling Language (JML) with temporal specifications. The extension is inspired by the patterns and specification language used within the Bandera project, and is especially tailored to specify properties of Java(Card) programs; for example, it allows the exceptional behaviour of methods to be specified. In the tradition of JML, the extension has been designed to be simple, easy and intuitive to use for software engineers. As an example, we show how the JML extension can be used to specify temporal aspects of the JavaCard API. Later, a semantics for the extension is discussed. We show how to translate a subset of the extension back into standard JML, thus allowing the re-use of existing verification techniques for JML. For the ‘new’ part of the language, a trace-based semantics is given.
Original languageEnglish
Title of host publicationAlgebraic Methodology and Software Technology, 9th International Conference, AMAST 2002, Saint-Gilles-les-Bains, Reunion Island, France, September 9-13, 2002, Proceedings
EditorsHélène Kirchner, Christophe Ringeissen
Number of pages15
ISBN (Electronic)978-3-540-45719-0
ISBN (Print)978-3-540-44144-1
Publication statusPublished - 2002
Externally publishedYes
Event9th International Conference on Algebraic Methodology and Software Technology, AMAST 2002 - Saint-Gilles-les-Bains, France
Duration: 9 Sept 200213 Sept 2002
Conference number: 9

Publication series

NameLecture Notes in Computer Science


Conference9th International Conference on Algebraic Methodology and Software Technology, AMAST 2002
Abbreviated titleAMAST 2002


Dive into the research topics of 'Extending JML Specifications with Temporal Logic'. Together they form a unique fingerprint.

Cite this