Software Download
Yoonsik Cheon | HOME


JML4c Overview | Download | Documentation

JML and Its Tools

The Java Modeling Language (JML) is a formal behavioral interface specification language for Java. It is used for detailed design documentation of Java program modules such as classes and interfaces. JML has been used extensively by many researchers across various projects and has a large and varied spectrum of tool support, extending from runtime assertion checking (RAC) to theorem proving. [more on JML ...]

Amongst these tools, RAC is one of the most widely used tool and translates JML specifications to runtime checks. However, lately there has been a problem for the JML RAC tool, known as the JML compiler (jmlc). The problem lies in its ability to keep up with new features being introduced by Java. The inability to support Java 5 features such as generics has been reducing the user base, feedback and the impact of JML usage. Another problem is the compilation speed of jmlc. On average, it is about nine times slower than a Java compiler such as javac. The jmlc tool uses a double-round strategy for generating RAC code. Its performance can be improved by optimizing compilation passes, in particular, by abandoning the double-round compilation strategy.

JML4c: A New JML Compiler

A new JML compiler (jml4c) uses a technique known as AST merging to improve compilation speed. The key idea is to parse the source code and its generated RAC code separately and to merge their parse trees. Thus, unlike its predecessor, jml4c parses the source code only once. Another feature of jml4c is that it was developed by extending the Eclipse Java compiler, and this will make it easy to support future changes in the Java language.

An experimental result shows that the AST merging technique on an average is about 1.6 times faster than the double-round strategy of jmlc; overall, jml4c is three times faster than jmlc. About 3500 JUnit test cases were newly created, and test cases and sample files from jmlc were incorporated. All the 35000 test cases for Eclipse were tested, and a subset of the DaCapo benchmark was also used to test the correctness and performance of the new compiler. Almost 1.5 million lines of code was compiled across 350 packages generating about 5000 class files.

The new JML compiler supports most of Level 0 and Level 1 features of JML. These are the features that are most commonly used when writing JML specifications.

API Specifications

Browse the API specifications of the JML4c implementation.

Technical Papers

For Local Developers

Last modified: $Id: doc.php,v 1.8 2010/03/21 03:12:17 cheon Exp $