JML Home Page
About JML
The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules. It combines the design by contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus.
The draft paper Design by Contract with JML (by Gary T. Leavens and Yoonsik Cheon) explains the most basic use of JML as a design by contract (DBC) language for Java.
The "white papers" below describe JML very briefly and some of its tools. The first of these gives a summary of all known tools. The second is a slightly dated summary of some of the main tools and how they relate to JML.
- Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer, 7(3):212-232, June 2005. [preprint PDF] (The original publication is available at http://www.springerlink.com from http://dx.doi.org/10.1007/s10009-004-0167-4.)
- Gary T. Leavens, K. Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs. JML: notations and tools supporting detailed design in Java. In OOPSLA '00 Companion, Minneapolis, Minnesota, pp. 105-106. Copyright ACM, 2000. Also Department of Computer Science, Iowa State University, TR #00-15, August 2000. [abstract] [postscript] [PDF]
Tools
From the download page you can get a set of open-source tools for work with JML. The most useful of these are an assertion-checking compiler (jmlc), a unit testing tool (jmlunit), and an enhanced version of javadoc (jmldoc) that understands JML specifications. See the papers above and the documentation for details.
People
The work on JML is a cooperative effort between:
- Gary T. Leavens's JML group at the University of Central Florida (formerly at Iowa State University).
- The developers of the MultiJava project.
- Yoonsik Cheon's group at University of Texas at El Paso.
- The LOOP verification project from Bart Jacobs's SoS group at the Radboud University Nijmegen. This group includes Erik Poll, and Joachim van den Berg.
- Joe Kiniry's group at University College Dublin.
- The ESC/Java2 project, led by Joe Kiniry and David Cok.
- Michael D. Ernst's group at MIT, which has produced the Daikon invariant detector and has worked on other tools and semantics relating to JML.
- Patrice Chalin's Dependable Software Research Group (DSRG), at Concordia University in Montreal, is working on language improvements (a new assertion semantics, non-null by default and arbitrary precision arithmetic) and their support in the Common (formerly ISU) JML tools and ESC/Java2. This group includes George Karabotsos and Perry James.
- David R. Cok (see pictures), who is an independent contributor, working at Kodak, who has worked on many tools, especially "jmldoc", "jmlspec", and ESC/Java2.
- The SpEx and JMLEclipse projects from the SAnToS Laboratory at Kansas State University, integrated by Matthew Dwyer, John Hatcliff, Robby, and Edwin Rodríguez. The SpEx project aims to extend JML to increase its suitability for the specification of concurrent programs. JMLEclipse is a JML front-end implemented as an Eclipse plugin.
- The KeY Project has theorem prover for Java Dynamic logic which includes a JML front end.
- Stephen Edwards's group at Virginia Tech, who are working on a tool that supports a wrapper approach to runtime assertion checking. This group includes Roy Tan.
- The Everest team at at INRIA Sophia Antipolis, which includes Gilles Barthe, Lilian Burdy, Julien Charles, Marieke Huisman, and Mariela Pavlova. This team has developed the JACK: Java Applet Correctness Kit environment and the Bytecode Modeling Language (BML), a bytecode variation of JML.
- Peter Müller at ETH Zurich and his students are working on the Universe type system. They also work on modular verification, including a treatment of frame axioms and a formal verification tool (Jive) that will use JML as its specification language.
- Arnd Poetzsch-Heffter and his students are working on modular verification, including a treatment of frame axioms and a formal verification tool (Jive) that will use JML as its specification language.
- David Naumann and his students are working on the semantics of JML and on using JML static verification tools to specify and check secure information flow properties.
- Claude Marché, Christine Paulin-Mohring, and Xavier Urbain in the Logical group at INRIA Futurs/Université Paris-Sud have produced the Krakatoa tool for verifying JML-annotated Java programs using the theorem prover Coq.
- The TFC (Constraint-based and Formal Techniques) group in Besançon works on Java/JML applications in two different directions. A testing activity, led by Bruno Legeard, works on adding JML/Java as an input to an existing framework for the symbolic animation and the automated test generation from formal models. A verification activity, led by Jacques Julliand, works on the automatic generation of JML annotations from proof obligations for verifying linear temporal properties.
- Tao Xie's group at North Carolina State University is working on testing and verification related projects.
- The Mobius project is a European Commission supported project that is using JML and developing "technology for establishing trust and security" using proof carrying code.
- The Extended Virtual Platform (XVP) project, directed by Suad Alagic, aims to support assertions at the virtual machine level.
- Christoph Csallner and Yannis Smaragdakis at Georgia Tech/University of Oregon.
- Frank Piessens's group at KU Leuven, Belgium, working on "concern-specific specification and verification to improve software quality and security." Besides Frank Piessens, this group includes Bart Jacobs (the younger).
- Timothy Wahls is working on execution of JML specifications (for rapid prototyping and debugging of specifications).
- Ricardo Massa F. Lima's group at the University of Pernambuco (UPE) in Brazil, which includes Henrique Rebêlo, who is working on adapting JML for Java Micro Edition (ME) applications).
- The Contract Guided System Development (ConGu) project is led by Professor Vasco Vasconcelos at the Universidade de Lisboa. This project aims to support the checking of Java classes against property-driven algebraic specifications.
- Daniel Jackson's Software Design Group, which includes Greg Dennis and Kuat Yessenov, who have developed JForge, a front-end to their Forge bounded verification library, that automatically analyzes Java code against full JML specifications.
- Although now disbanded, an important original group working on JML was the former extended static checking project (which includes ESC/Java) at HP SRC Classic (formerly Compaq Systems Research Center). This group included K. Rustan M. Leino, Cormac Flanagan, Mark Lillibridge, Greg Nelson, Raymie Stata, James B. Saxe.
JML is an open project, and we welcome the participation of other groups. If your group is working on JML but not listed above, please send an email to Gary Leavens.
Development of JML is hosted on sourceforge.net.
Last modified Tuesday, January 8, 2008.