Software Download
Yoonsik Cheon | HOME
JET | JML4c | UTJML | BibPHP | JML
|
|
Software Download
|
JET | JML4c | UTJML | BibPHP | JML |
|
|
|
JML4c
|
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.
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.
Browse the API specifications of the JML4c implementation.
Last modified: $Id: doc.php,v 1.8 2010/03/21 03:12:17 cheon Exp $