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 papers below describe JML very briefly and some of its tools. The paper Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2 (by Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll) contains a description of JML and its tools that is suitable for those who are already more familiar with the idea of assertions. The second gives a summary of all known tools.
- Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll. Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. In Formal Methods for Components and Objects (FMCO) 2005, Revised Lectures, pages 342-363. Volume 4111 of Lecture Notes in Computer Science, Springer Verlag, 2006. [Corrected preprint PDF] (The original publication is available at springerlink.com or directly from http://dx.doi.org/10.1007/11804192_16.)
- 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.)
Tools
From the download page you can choose between several open-source tools for using 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).
- David R. Cok (see pictures), who is an independent contributor, once working at Eastman Kodak, GrammaTech and AdaCore, now an independent consultant for international firms on software correctness. David has worked on many tools, especially OpenJML, "jmldoc", "jmlspec", and ESC/Java2.
- The KeY Project has theorem prover for Java Dynamic logic which includes a JML front end.
- Yoonsik Cheon's group at University of Texas at El Paso.
- The former developers of the MultiJava project (especially Curtis Clifton).
- The LOOP verification project from Bart Jacobs's SoS group at the Radboud University Nijmegen. This group includes Erik Poll and, over the years, Joachim van den Berg, Marieke Huisman, Engelbert Hubbers, Joe Kiniry, Martijn Oostdijk, Martijn Warnier, and several other contributors.
- Joe Kiniry at Galois.
- The ESC/Java2 project, led by Joe Kiniry and David Cok.
- Michael D. Ernst's group at the University of Washington, which has produced the Daikon invariant detector and has worked on other tools and semantics relating to JML and Java, including testing tools, work on Java's type annotations (JSR 308), and the Checker Framework.
- Patrice Chalin, formerly at Concordia University in Montreal, who worked on various JML improvements (including a new assertion semantics, non-null by default and arbitrary precision arithmetic) and their support in the Common (formerly ISU) JML tools.
- Researchers in the SAnToS Laboratory at Kansas State University, which included Matthew Dwyer, John Hatcliff, Robby, and Edwin Rodríguez, who worked on the SpEx project, that aimed to extend JML to increase its suitability for the specification of concurrent programs and developed a JML front-end as an Eclipse plugin.
- Stephen Edwards's group at Virginia Tech, who worked on a tool that supported a wrapper approach to runtime assertion checking.
- Marieke Huisman and collaborators in the Formal Methods and Tools Group at the University of Twente, Netherlands. Before, Marieke was part of the Everest team at INRIA Sophia-Antipolis, that developed the JACK: Java Applet Correctness Kit environment and the Bytecode Modeling Language (BML), a bytecode variation of JML.
- Jacek Chrzaszcz and others at the Institute of Informatics of Warsaw University, Poland, who develop tools for BML.
- The Imdea Software group in Madrid, Spain, including Gilles Barthe, and Anindya Banerjee.
- Peter Müller at ETH Zurich and his students worked on the Universe type system, and continue to work on modular verification issues.
- Arnd Poetzsch-Heffter and his students worked 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 worked 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 others in the Toccata group at the INRIA Saclay - Ile-de-France research center, the CNRS and the University of Paris-Saclay, produced the Krakatoa tool for verifying JML-annotated Java programs using the theorem prover Coq.
- Tao Xie's group at the Univ. of Illinois has worked on testing and verification related projects.
- The Extended Virtual Platform (XVP) project, directed by Suad Alagic, aims to support assertions at the virtual machine level.
- Christoph Csallner at University of Texas at Arlington.
- Frank Piessens and Bart Jacobs's group at KU Leuven, Belgium, worked on "concern-specific specification and verification to improve software quality and security."
- Timothy Wahls worked on execution of JML specifications (for rapid prototyping and debugging of specifications).
- Henrique Rebêlo, who has developed several projects related to runtime assertion checking of JML, including AspectJML a tool that can specify and do runtime assertion checking for both Java and AspectJ programs.
- The Contract Guided System Development 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 developed JForge, a front-end to their Forge bounded verification library, that automatically analyzes Java code against full JML specifications.
- Software Productivity Group at the Federal University of Campina Grande (UFCG), Brazil, which includes Rohit Gheyi, Tiago Massoni, Catuxe Varjão and Laerte Xavier, are implementing and evaluating a Java/JML conformance checking tool.
- The VeriFlux product from aicas used JML for generating Loop bounds for Worst Case Execution Time Analysis.
- Daniel M. Zimmerman, who created JMLUnitNG.
- The XJML project is an extensible front-end for JML that has the ability to process preconditions, posconditions, and class invariants using JML and XML in separate files. It can also do runtime assertion checking or extended static checking.
- Néstor Cataño and his group are working on several JML projects including an Event B to JML plugin for Rodin, B2JML a tool that translates B machines into JML, and a Rodin plug-in EventB2Java that generates JML-specified Java implementations of Event-B machines.
- 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 (leavens@ucf.edu).
Development of JML is hosted on github.com.
Last modified Friday, December 10, 2021.