One area of future work for JML is concurrency.
The main feature currently in JML that supports concurrency is the
clause [Lerner91] [Sivaprasad95]; it says that the caller will be delayed
until the condition given holds.
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.
JML also has several primitives from ESC/Java that deal with monitors
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 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 and CCR-0113181.
Many people have helped with the semantics and design of JML, and on this document. Thanks to Yoonsik Cheon, Bart Jacobs, Rustan Leino, Peter Müller, Erik Poll, 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, 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, Abhay Bhorkar, Marko van Dooren, Anand Ganapathy, Yogy Namara, Todd Millstein, and Arun Raghavan 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, and Arthur Thomas for help with case studies and specifications in JML. Thanks to Judy Chan Wai Ting, Peter Chan, Marko van Dooren, Fermin da Costa Gomez, Joseph Kiniry, Roy Patrick Tan, 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 in Fall 2002 for suggestions and comments about JML.
Go to the first, previous, next, last section, table of contents.