OpenJML (JML)

Eclipse plug-in for OpenJML

This page provides installation instructions and a brief overview of the functionality of the OpenJML Eclipse plugin. More detailed information about the plugin is available in the Help documentation that is installed with the plugin.

Installing

OpenJML provides a standard Eclipse plug-in update site at http://jmlspecs.sourceforge.net/openjml-updatesite. The plug-in is supported for current versions of the Kepler and Luna releases (Juno generally works but is deprecated). The installation procedure is standard for Eclipse:

• Select the menu option Help >> Install New Software
• Click Add...
• Enter OpenJML as the Name and the URL given above as the Location, and press OK.
• Select the most recent version of OpenJML from the list, and press Next
• Review your selections and press Next
• Read and accept the license agreements and press Finish
• Restart Eclipse

These instructions may vary slightly on other Eclipse versions or on MacOS platforms.

To enable JML functionality, you will need to do these additional tasks:

• For each project of interest, select the project name in the Package Explorer View and then the JML >> Enable JML for project menu action.
• On the OpenJML Solvers preference page, select a default solver and enter the path to the solver executable.
• On the OpenJML preference page, select the 'Skip Purity Check' option.

[TBD - Add a description of installation using the dropins folder]

Features

[TBD - this section needs review and updating]

Menubar and toolbar items

The Menubar and toolbar contain these additional items:

• The JML menubar entry with its submenu items.
• A toolbar item marked by the JML logo (a yellow coffee cup), which initiates type-checking of a Java or JML file.
• A toolbar item marked ESC, which initiates static checking of selected files, classes or methods.
• A toolbar item marked RAC, which initiates compilation for runtime assertion checking.

The JML sub-menu items are described in detail in the Help documentation. Note that the same menu actions are available from the 'JML' item on the main menubar, from context menus in Package Explorer, Navigator, and Outline (and perhaps other) Views. The menu actions provide the following groups of functionality:

• enabling and disabling JML on a project
• typechecking all or a selected set of files
• static checking all or a selected set of files, or individual methods
• applying runtime assertion compilation to all or a selected set of files
• adding or removing files from the set of files that are automatically RAC-compiled
• viewing and editing the sourcepath and specspath
• showing counterexample model information generated by a (failed) attempt to validate a method
• showing the composite (including inherited) specs for a method
• opening an editor on the .jml file corresponding to a .java file
• cleaning up errant JML problem markers

JML Nature and automatic building

By enabling JML for a project (select a project and then activate the 'Enable JML' menu item), you add the Eclipse JML Nature to the project (along with the Java Nature for the project). When JML is enabled, the project icon in the Package Explorer and other Views is decorated with the JML logo (the yellow coffee cup) in its upper right. More importantly, OpenJML type-checking of files is automatically performed whenever the file is built by the Java compiler. Thus if you have 'Build Automatically' enabled for the project, then any file is compiled whenever it is saved; if the JML Nature is enabled, the file will also be type-checked by OpenJML whenever it is saved. Note that OpenJML only operates on the saved version of the file, not on the content of an unsaved (dirty) editor.

You can also enable automatic Runtime Assertion Compilation or Extended Static Checking for files upon saving. These are not enabled by default. More detail is provided about the appropriate use of these features in the Help documentation.

JML problem markers

The OpenJML plugin converts problems reported by OpenJML into Eclipse Problem Markers, with all the functcionality such markers have in Eclipse:

• The markers are displayed in editors
• The appearance of the markers can be customized using the options on the Preference page at General>>Editors>>Text editors>>Annotations. You can turn the markers on and off in either the left or right rulers and change the color and style (highlight or squigglies) of the marker.
• The OpenJML errors and warnings are listed in the Problem View. The Problems have a category (JML) enabling the Problem View to customize when they are to be displayed in the View's list.

JML Console

OpenJML contributes an additional kind of Console (the JML Console) to Eclipse. Various textual information will be written to the console as OpenJML operations are executed. The amount of information can be controlled by options on the OpenJML Preferences page. The information is in large part the same information that is produced by the OpenJML command-line tool, augmented with some information about the operation of the plugin itself.

File association for .jml files and the Java editor

The plugin creates a new content type for .jml files and associates it with the Java editor. So you can double-click a .jml file to open an editor and all the Java editing capability is available for .jml files.

However, since we are using a standard Java editor, there is no special knowledge of JML syntax. It is a future work item to extend the Java editor to be JML-aware. Note that the Eclipse Java compiler is still active, even when the OpenJML compiler is present to do JML checkin.

Consequently the Java compiler will issue errors about some legitimate JML features:

• JML files may contain class declarations even though the suffix is not .jml.
• Method declarations in JML files do not have bodies (even though they are not abstract).
• Final field declarations in JML files are not initialized.

Preferences

The OpenJML plugin contributes a typical Preferences Page to the Eclipse preferences menu. It is accessed through the top-level 'OpenJML' item in the Preferences outline.

There are two preference pages -- a main one with most of the individual options and a subsidiary page on which paths to solvers are set. The subsidiary page is seen by opening up the twisty by the OpenJML item in the Preferences outline.

The Preference options correspond to the options available in the command-line tool, discussed here. There are a few points to note:

• One must specify the solver to use for ESC on the Solvers page, as well as the paths to the executables of any solver intended to be used.
• The command-line tool uses option settings taken from a openjml.properties file. An Eclipse plug-in has its own, separate properties persistence mechanism. So the Eclipse plugin does not use the openjml.properties file. However, there is a button on the preferences page: clicking it will set the preferences by loading them from the openjml.properties page. This can be used as a one-time initialization of the Eclipse preferences.

Commands and key associations

All actions (i.e., responses to menu selections) contributed by the OpenJML plugin are associated with Eclipse Commands. Thus they appear in the list of commands on the General>>Keys preference page and can have keyboard bindings associated with them.

Eclipse help

Conventional Eclipse Help about the OpenJML plugin is available from Eclipse's Help>>Help Contents menu item.

Last modified Nov 14 2025.