The Java Modeling Language (JML)

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).
• 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, over the years, Joachim van den Berg, Marieke Huisman, Engelbert Hubbers, Joe Kiniry, Martijn Oostdijk, Martijn Warnier, and several other contributors.
• Joe Kiniry's KindSoftware group at the IT University of Copenhagen. (The group was at University College Dublin from 2004-2009.) This group includes or included contributors Julien Charles, Dermot Cochran, Vieri del Bianco, Eva Darulova, Fintan Fairmichael, Radu Grigore, Clement Hurlin, Mikolas Janota, Josu Martinez, Alan Morkan, Dragan Stosic, and many others.
• 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'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, once working at Eastman Kodak, now working at GrammaTech, who has worked on many tools, especially OpenJML, "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.
• 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 Aleksy Schubert, 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 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 at University of Texas at Arlington.
• 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).
• The JML AOP project, in Ricardo Massa F. Lima's group at the Federal University of Pernambuco (UFPE) in Brazil. This includes Henrique Rebêlo, who is also working on adapting JML using aspect-oriented programming.
• 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.
• The Relational Formal Methods Research Group (RFM) led by Marcelo Frias does research aimed at several areas of software engineering, such as formal language design, language analysis, software verification and validation, and automated generation of test cases. They have developed TACO, a tool that automatically analyzes a JML specification using a SAT-solver as a backend.
• 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 CHARTER project, which is using JML for certification. This project is both building specifications for essential Java classes and the RTSJ (Radbound Universiteit Nijmegen) and is using JML for automatic test generation (Chalmers).
• The VeriFlux product from aicas uses JML for generating Loop bounds for Worst Case Execution Time Analysis.
• Daniel M. Zimmerman the author of 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@eecs.ucf.edu).

Development of JML is hosted on sourceforge.net.

We have yearly workshops on JML. The 2017 workshop on JML is hosted at UCF by Gary Leavens.

Last modified Thursday, December 14, 2017.