Information Technology Reference
In-Depth Information
4.2
Strengthening JML Annotations
We can use the same approach to the JML specifications available for the Java
libraries. What we did here with HashMap and part of the JML type system could
be done again for other parts of the Java Development Kit (JDK), and this has
already been done before for AbstractCollection with positive results [17].
The research community can now take the opportunity to systematically verify
the JML specification of the entire JDK, and the same could be said for the
JML specifications of other frameworks, such as the Java cards API [29,39].
Another interesting point about linking Z and JML in this way is that we
can draw inspiration from concrete implementations specified in JML up to Z
specifications of similar concepts. That is exactly what happened in the work
done in [11,10]. We started by mechanising a well-known abstract specification
of a filing system given in [26], assumed that a hash map would be a good imple-
mentation candidate and started doing the concrete specification. At this point,
when we needed to think how to model a hash map in Z, we drew inspiration
from the available JML specification for the Java HashMap class. This was also
helpful in finding the right retrieve relation to prove the refinement between ab-
stract and concrete Z specifications. The same route could be repeated for other
important data types.
4.3
JML to Z
A step forward beyond verification of class libraries and frameworks would be
the verification of the JML semantics itself. This would provide a basis for a logic
for reasoning about JML specifications. For that we need more than what Z of-
fers: the specification of abstract data types. JML has specification facilities for
real-time, concurrency, and resource allocation, which could be captured within
Hoare and He's Unifying Theories of Programming [14]. As mentioned above,
JML is divided into language levels [24, Sect. 2.9], where there are minimum,
desirable, and “exocentric” language features to be considered. The behavioural
part that Z can capture is definitely the very basic/core part of JML, hence the
most obvious place to start. The next step would be to combine JML concur-
rency features with Java models for CSP, which are also already available. The
obvious path is the to add a systematic formal translation from JML to these
different formalisms. Although this is a more ambitious project, it is a feasible
(and promising one) nevertheless.
4.4
Z to JML
The other way round, from concrete Z specifications down to JML specifications,
would also be very interesting. It would enable the prototyping of Z specifications
in Java, which we believe will be attractive. There is already ongoing work in
this direction in Community Z Tools (CZT). 3
Another interesting possibility
3 See czt.sourceforge.net .
 
Search WWH ::




Custom Search