6. Future Work and Conclusions

One area of future work for JML is concurrency. Our current plan is to use when clauses that say when a method may proceed to execute, after it is called [Lerner91] [Sivaprasad95]. This permits the specification of when the caller is delayed to obtain a lock, for example. While syntax for this exists in the JML parser, our exploration of this topic is still in an early stage. We may also be able to expand history constraints to use temporal logic.

Another area for future work on JML is to synthesize the previous work of Wahls, Leavens and Baker on the use of constraint logic programming to directly execute a significant and practical subset of JML's assertions [Wahls-Leavens-Baker98]. This prior work supports the "construction" of post-state values to satisfy ensures clauses, including such clauses containing quantified assertions. Successful integration of these assertion execution techniques with JML would support automatic generation of Java class prototypes directly from their JML specifications.

In conclusion, JML combines the best features of Eiffel and the Larch approaches to specification. This combination, we believe, makes it more expressive than Eiffel, and more practical than Larch style BISLs as a tool for recording detailed designs.

More information about JML can be found on the web at the following URL.
`http://www.jmlspecs.org/'

Acknowledgments

Thanks to Rustan Leino and Peter Müller for many discussions about the semantics of such specifications and verification issues relating to Java. For comments on JML we thank Peter, Jianbing Chen, Anand Ganapathy, Sevtap Oltes, Gary Daugherty, Karl Hoech, Jim Potts, and Tammy Scherbring. Thanks to Anand Ganapathy for his work on the type checker used to check our specifications.

The work of Leavens and Ruby was supported in part by a grant from Rockwell International Corporation and by the US NSF under grant CCR-9503168. The work of Leavens, Baker, and Ruby is supported in part by NSF grants CCR-9803843, CCR-0097907 and CCR-0113181.

This paper is adapted from Haim Kilov, Bernhard Rumpe, and William Harvey (editors), Behavioral Specifications for Businesses and Systems, chapter 12, pages 175-188. Copyright (C) Kluwer Academic Publishers, 1999. Used by permission.

Thanks to Faraz Hussain for comments on recent versions of this paper that resulted in some clarifications with respect to recent features of JML.