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 instructions for installation are given here.

[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 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:

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:

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:

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:

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.