JML4PluginExplanation

ESC/Java2 is currently being maintained to support new verification functionality, but its compiler frontend has yet to support Java 5 source code.

JML4 is a customization of the Eclipse subsystem that support Java program development, the Java Developers Toolkit org.eclipse.jdt. JML4 provides runtime assertion checking and has extension points which are used by other subsystems, like a customized bridge that connects ESC/Java2 to JML4 (CJK07).

JML4 currently enhances Eclipse versions 3.3 to 3.4 with:

• scanning and parsing of nullity modifiers,
• enforcement of the JML non-null type system, both statically and at runtime, and
• item the ability to read and make use of the extensive JML API library specifications.

This subset of features was chosen so as to exercise some of the basic capabilities that any JML extension to Eclipse would need to support.

These include

• recognizing and processing JML syntax inside specially marked comments, both in .java files as well as .jml files;
• storing JML-specific nodes in an extended AST hierarchy,
• statically enforcing a modified type system, and
• providing for runtime assertion checking (RAC).

Also, the functionality added by the chosen subset of features is useful in its own right, somewhat independent of other JML features; i.e. the capabilities form a natural extension to the existing embryonic Eclipse support for nullity analysis.

JML4 development continues, led by Concordia University, and mainly supported by an NSF Infrastructure grant in the U.S.A. A JML4 "bootcamp" took place in Florida in the first quarter of 2008. At that event developers from all over the world, including MOBIUS-funded researchers, were introduced to the design and development of the JML4 plugin.

It is expected that the first public release of JML4 will take place in 2008 and will support all of JML level 0 and level 1. These technical issues (the level of JML support and rich Eclipse integration) as well as social aspects (the size and activity level of the JML community working on/with JML4) means that JML4 is a strong candidate as a frontend for future MOBIUS tools.

The current status of JML4 is shown in the JML4 wiki: [http://jmlspecs.wiki.sourceforge.net/JML4] and in the JML Reloaded mailing list.

Version: 3 Time: Fri Mar 28 14:29:57 2008 Author: dcochran (dcochran) IP: 193.1.132.32