Extending JML Specifications with Temporal Logic
| Autor: | Kerry Trentelman, Marieke Huisman |
|---|---|
| Rok vydání: | 2002 |
| Předmět: |
Application programming interface
Java Computer science Programming language Semantics (computer science) Specification language computer.software_genre TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Temporal logic Java Card computer TRACE (psycholinguistics) computer.programming_language Java Modeling Language |
| Zdroj: | Algebraic Methodology and Software Technology ISBN: 9783540441441 AMAST |
| DOI: | 10.1007/3-540-45719-4_23 |
| Popis: | This paper proposes an extension oft he 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 ofe xisting verification techniques for JML. For the 'new' part of the language, a trace-based semantics is given. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|