JML2 Eclipse Plug-In

Overview

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

Originally, this plug-in started as a small part of the Universe type system inference tools, but was spun off later. See the research page for an overview of the Universe type system and the tools page for information about the tools we provide.

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 documentation and examples 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

Also see the "JML2 Eclipse plug-in" category in the SF Tracker. Please add any bugs and feature requests there.

• Caching of files is broken in JML2, especially if switching between checker and RAC or between different projects. Restarts seem to be the only workaround so far. See [2122537].
• "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

Contact

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 MultiJava and JML2 are available from their respective web sites. Also see the GNU General Public License, version 2.

Werner M. Dietl

Release History

Release History

Version 1.1.1, November 5th 2008:

• Fixed error resource look-up, especially for JML specification files and Windows systems.
• Fixed checking of dirty editor state.
• Fixed parsing of UTS checker property, now spaces are stripped.

Version 1.1.0, September 22nd 2008:

• Error message parsing improved, in particular, the error markers are always put on the correct file now.
• The "JML2 Error View" now allows to directly jump to the error.
• Moved the "JML2 Error View" into the "Java" category.
• The JML2 checker project nature can now be turned on or off using the project properties page.
• Renamed packages from ".sct." to ".pm.".
• Many small cleanups, removed all Eclipse and FindBugs warnings.

Version 1.0.9, August 8th 2008 (08.08.08):

• Auto-build support: added a project nature that automatically runs the JML2 checker in the background.
• Optional status messages make it easier to see what auto-build is doing. A top-level plug-in property can be used to turn these messages off.
• Improved the activation of the toolbar buttons.
• Split into two features: plug-in and help.
• Added the command line names to the properties page for easier reference with the manual page. Added "Xlint" and "xArrayNNTS" support.
• Improved the about messages.

Version 1.0.8, July 20th 2008:

• Use the background task system of Eclipse now. If you don't see anything happen, look into the "Progress" view.
• Completely changed how the classpath is computed. Now we simply use the project classpath. Usually, you should not need to specify a classpath or sourcepath in the checker properties.
• Removed the jml-runtime.jar file and always use jmlrelease.jar, also for RAC execution.
• Added three toolbar buttons. Creative spirits can feel free to send nicer icons.
• Wasted time on adding keyboard shortcuts, until I found a bug report. With the top-level toolbar also the keyboard shortcuts work now.
• Added the manual pages to the help system.

Version 1.0.7, July 16th 2008:

• Fixed a problem with the RAC launch configuration.
• Included the JML Exec runtime files, this should now fully support JML Exec.

Version 1.0.6, July 14th 2008:

• Re-designed the property pages, removing redundancy between checker and compiler.
• First support for the JML Exec tool. Feedback needed on what else should be added.
• Included JML reference manual, preliminary design, and design-by-contract with JML in the Eclipse Help system. Try Help -> Help Contents.
• Added easier keyboard navigation.
• Added jmli, jmll, and jmlh code completion templates for invariants, lightweight, and heavyweight method specifications, respectively. To prevent automatic re-formating from Eclipse, one has to manually make the inserted code a comment. However, this still saves a lot of typing. Suggestions for better or more templates welcome.
• Many code cleanups, now compiles without a warning using Eclipse 3.4.
• Re-compiled everything with Java 5.
• Updated MJ/JML2 sources.

Version 1.0.5, February 2008:

• Updated MJ/JML2 with better GUT support.
• Plug-ins use Java 5 generics now.
• Source files in packages should work.
• Redrawing of error messages and markers improved. Try copy-pasting a JML error a few hundred times.

Version 1.0.4, October 2007: Small improvements.

Version 1.0.2, March 2007: Improvements during the master project of Andreas Fürer

Version 1.0.0, Summer 2006: Semester project of Paolo Bazzi