Voltar
Capítulo de livro Revisado por pares
BIBTEX RIS

Extending JML Specifications with Temporal Logic

2002; Springer Science+Business Media; Linguagem: Inglês

10.1007/3-540-45719-4_23

ISSN

1611-3349

Autores

Kerry Trentelman, Marieke Huisman,

Tópico(s)

Logic, programming, and type systems

Resumo

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.

Referência(s)