Résumé:
This talk presents work done in collaboration with Marieke Huisman on
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. An
example will be given, showing how the JML extension can be used to
specify temporal aspects of the JavaCard API. It will also be shown
how a subset of the extension can be translated back into standard
JML, thus allowing for the re-use of existing verification
techniques. A state-based semantics will be given for the "new" part
of the language.
Retour au sommaire / Back to schedule