JML Eclipse Plugin

This Eclipse plug-in provides a basic integration of the external pageCommon JML2 tools into the external pageEclipse IDE.

Installation

Add the URL

http://www.pm.inf.ethz.ch/research/universes/tools/eclipse/

as an update site to Eclipse. Then search for new plug-ins and install the JML2 Eclipse plug-in. We provide two Eclipse "features": the main plug-in for all tools and a help plug-in. These two are independent of each other and can be installed as needed.

Requirements

The plug-in was developed using Sun Java 6 and Eclipse 3.4.1 on Linux. However, the plug-in and the included JML2 were compiled to Java 5 bytecode and should therefore run with an older JVM.

Basic Usage

After successful installation, you will find the following changes: 1) a "JML2 Tools" context menu and toolbar buttons, 2) a "Run As -> JML Rac" configuration, and 3) "JML2 Plug-in" properties page in the project properties.

In the "Project Explorer", the context menu for files and folders contains a "JML2 Tools" sub-menu with three commands: 1) "Run JML2 checker" executes the static type checker and 2) "Run JML2 compiler" checks the code and then compiles it with runtime assertion checking (RAC). 3) "Run JML2 exec" checks the code and then compiles it with the JML exec tool.

Code that has been compiled with RACs can be executed with "Run As -> JML Rac". If a runtime check fails the exception is printed in the "Console" view.

The project properties contain a "JML2 Plug-in" page that sets the command line options for the checker and the compiler.

The toolbar can be enabled by selecting the "Window -> Customize Perspecitve..." menu, then selecting the "Commands" tab and then enabling the "JML2 plug-in toolbar" option.

The default keyboard shortcuts can be changed by selecting the "Window -> Preferences..." menu, then selecting the "Keys" tab under "General" and then configuring the "JML2..." entries.

See the JML2 external pagedocumentation and external pageexamples for details about JML.

Feature Summary

Executing the JML2 checker, RAC compiler, and exec tool using a context menu command, a toolbar button, or a keyboard shortcut.
Project properties pages to configure the tools. Java project properties are automatically used for the JML2 tools.
Code completion templates make adding JML comments easier.
Execute an application with RAC support.
JML2 Error View displays the messages from the tools.
Auto-build support to automatically run the JML2 checker on edited files.
Status messages and progress reports.
Help system includes the JML reference manual and papers.

Screenshots

Main Eclipse window with JML2 Error View

JML2 checker properties page

Help page

Open Issues

Caching of files is external pagebroken in JML2, especially if switching between checker and RAC or between different projects. Restarts seem to be the only workaround so far. See [external page2122537].
"Linked" projects don't work. When you import a project, make sure that the files are located within your workspace directory, e.g. by selecting to copy the files. Otherwise the way the plug-in calculates the classpath will fail and the project will not compile.
Tighter integration into the help system could be done, e.g. by providing an index and links from the different dialog windows.

Tested Environments

Version 1.1.0 was successfully tested in the following environments:

Linux (Red Hat WS 5, Ubuntu 8.04, Fedora Core 6)
Mac OS X 10.5.4
Windows XP

Disclaimer

These tools are provided as-is without any support or warranty. The source code for the plug-ins is contained within the respective JAR files. The source code for external pageMultiJava and external pageJML2 are available from their respective web sites. Also see the external pageGNU General Public License, version 2.

Acknowledgment

The JML Eclipse plug-in was developed by external pageWerner Dietl.