4. Conclusions

One area of future work for JML is concurrency. Some recent work by Rodriguez et al. [Rodriguez-etal05] has investigated the use of atomicity for specifying multi-threaded Java programs. However, these ideas are not yet implemented in most of the JML tools, and their use has not been fully explored.

JML has also been used as a research vehicle in a wide variety of other studies various papers on these ideas can be found through the JML web page `http://www.jmlspecs.org/'.

JML is an expressive behavioral interface specification language for Java. It combines the best features of the Eiffel and Larch approaches to specification. It allows one to write specifications that are quite precise and detailed, but also allows one to write lightweight specifications. It has examples and other forms of redundancy to allow for debugging specifications and for making rhetorical points. It supports behavioral subtyping by specification inheritance.

More information on JML, including software to aid in working with JML specifications, can be obtained from `http://www.jmlspecs.org/'. The JML web site also includes an up-to-date version of this document with a table of contents and an index.

Acknowledgments

The work of Leavens and Ruby was supported in part by a grant from Rockwell International Corporation and by NSF grant CCR-9503168. Work on JML by Leavens, Baker, and Ruby was also supported in part by NSF grant CCR-9803843. Work on JML by Leavens, Ruby, and others is supported in part by NSF grants CCR-0097907,CCR-0113181, CCF-0428078, and CCF-0429567.

Many people have helped with the semantics and design of JML, and on this document. Thanks to Yoonsik Cheon, David Cok, Bart Jacobs, Rustan Leino, Peter Müller, Erik Poll, Arnd Poetzsch-Heffter, and Joachim van den Berg, for many discussions about the semantics of JML specifications. Thanks to Raymie Stata for spear-heading an effort at Compaq SRC to unify JML and ESC/Java, and to Rustan and Raymie for many interesting ideas and discussions that have profoundly influenced JML. For comments on earlier drafts and discussions about JML thanks to Yoonsik, Bart, Rustan, Peter, Eric, Joachim, Raymie, Abhay Bhorkar, Patrice Chalin, Curtis Clifton, John Boyland, Martin Büchi, Peter Chan, David Cok, Gary Daugherty, Jan Docxx, Marko van Dooren, Stephen Edwards, Michael Ernst, Arthur Fleck, Karl Hoech, Marieke Huisman, Anand Ganapathy, Doug Lea, Claude Marche, Kristof Mertens, Yogy Namara, Sevtap Oltes, Arnd Poetzsch-Heffter, Jim Potts, Arun Raghavan, Alexandru D. Salcianu, Jim Saxe, Tammy Scherbring, Tim Wahls, Wolfgang Weck, and others we may have forgotten. Thanks to David Cok, Yoonsik Cheon, Curtis Clifton, Patrice Chalin, Abhay Bhorkar, Kristina Boysen, Tongjie Chen, Kui Dai, Werner Dietl, Marko van Dooren, Anand Ganapathy, Yogy Namara, Todd Millstein, Arun Raghavan, Frederic Rioux, Roy Tan, and Hao Xi for their work on the JML checker and tools used to check and manipulate the specifications in this document. Thanks to Katie Becker, Kristina Boysen, Brandon Shilling, Elizabeth Seagren, Ajani Thomas, and Arthur Thomas for help with case studies and specifications in JML. Thanks to David Cok, Joe Kiniry, Yoonsik Cheon, Kristina Boysen, Curtis Clifton, Judy Chan Wai Ting, Peter Chan, Marko van Dooren, Kui Dai, Fermin da Costa Gomez, Joseph Kiniry, Roy Patrick Tan, and Julien Vermillard for bug reports about JML tools. Thanks to the students in 22C:181 at the University of Iowa in Spring 2001, and in Com S 362 at Iowa State University for suggestions and comments about JML.