Abstract
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 language | English |
|---|---|
| Title of host publication | Algebraic Methodology and Software Technology, 9th International Conference, AMAST 2002, Saint-Gilles-les-Bains, Reunion Island, France, September 9-13, 2002, Proceedings |
| Editors | Hélène Kirchner, Christophe Ringeissen |
| Publisher | Springer |
| Pages | 334-348 |
| Number of pages | 15 |
| ISBN (Electronic) | 978-3-540-45719-0 |
| ISBN (Print) | 978-3-540-44144-1 |
| DOIs | |
| Publication status | Published - 2002 |
| Externally published | Yes |
| Event | 9th International Conference on Algebraic Methodology and Software Technology, AMAST 2002 - Saint-Gilles-les-Bains, France Duration: 9 Sep 2002 → 13 Sep 2002 Conference number: 9 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 2422 |
Conference
| Conference | 9th International Conference on Algebraic Methodology and Software Technology, AMAST 2002 |
|---|---|
| Abbreviated title | AMAST 2002 |
| Country/Territory | France |
| City | Saint-Gilles-les-Bains |
| Period | 9/09/02 → 13/09/02 |