Proving Theorems About JML Classes - Formal Methods and Hybrid Real-Time Systems - page 277

is to have JML as a target language for the refinement calculus [25] (or even
the Z refinement calculus [6]). As there are available refinement tools for the
refinement calculus that have other target languages rather than Java, we think
this is also a profitable way forward.
This is a more modest endeavour than going from JML to Z, yet there are
still interesting issues to tackle. One example is the treatment of undefined ex-
pressions in JML. Moreover, some of the quite powerful abstraction mechanisms
available in Z would be dicult to directly translate to JML, like given sets and
loosely defined paragraphs. Like in [37], we would obviously need to adhere to
some Z specification patterns prior to translation to JML.
An important issue still to be considered in such a development is how to
tackle the object-oriented features of JML. One could argue that Object-Z [33]
would be a better candidate to aim for. Nevertheless, as there is no agreeable
notion of refinement for Object-Z, we would rather prefer to stick to Z itself,
perhaps using the solutions already described in [38].

4.5 Finally

In this paper we emphasise the benefits of proving theorems about JML specifi-
cations using the Z notation. We focus on the specification of the Java HashMap
class, and parts of the JML meta-type system classes. This reveals interest-
ing opportunities to improve JML specifications, uncovering some problems and
strengthening the JML specifications with theorems from Z.
In linking Z and JML, we are paving the way towards providing formally
documented components for the Verified Software Repository that others will
find useful. Java's HashMap architect Joshua Bloch once said [2]
Writing reusable software components is a bit like being a plumber. It's
a critical but largely thankless task. No one says, “Gosh, your plumbing
is really great!” But you can bet they would complain if it leaked.

Acknowledgements

We would like to thank the Software Assurance Group at QinetiQ Malvern for their
long-term funding and support for our research group. We are grateful to Zheng
Fu for his work with the formalisation of a Z hash map for a POSIX filing system
specification and verification. Finally, we are grateful to Gary Leavens and the JML
community list for the various discussions during the development of the paper.

References

1. Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction. In:
Graduate Texts in Computer Science, Springer, Heidelberg (1998)
2. Bloch, J.: Effective Java Programming Language Guide. Prentice Hall, Englewood
Cliffs (2001)