Résumé:
We have worked in JML: a specification language tailored to
Java. JML
allows us to define the functional behaviour of methods: pre-conditions
and post-conditions, and apart from that, class
invariants. Unfortunately, using only the functional specification of a
method is not enough to reason about arbitrary method
invocations. Therefore, "modifiable" clauses are introduced. The
"modifiable" clause in a method represents the set of variables
which it may modify. There are several projects using "modifiable"
clauses, for example: JML
and Esc/Java(an subset of JML) define an
specification of the modifiable clauses, but its implementation
presents some problems. In the LOOP project is defined an
implementation of some JML pragmas, including the modifiable
one. This implementation is based on its underlying memory model and the
logic representation of Java and the JML constructs. This
implementation is not easy and fast method for its verification
yet. We present a first solution to achieve this in a context without
"aliasing". For this specification we have done
an implementation, which have extended some functionalities of the
JML parser. Our approach presents some advantages on
LOOP project approach, namely: is faster than it and the
verification is closer to the specification language. "The
electronic banking case study" is used to demonstrate the usability of
our approach.
Retour au sommaire / Back to schedule