JML Eclipse Plugin
Author: David Cok
1 December 2012
Feedback
This plugin provides JML functionality integrated with Eclipse (4.2) UI for Java 1.7.
It is a GUI interface to the OpenJML command-line tool.
Contents:
This plug-in provides Java Modeling Language
(JML)
functionality as an Eclipse plug-in into the Java development environment of Eclipse.
The JML plug-in
in particular provides functionality for checking and manipulating formal specifications
of Java programs. The plug-in works with Eclipse 4.2 (tested with 4.2.1); the
back-end OpenJML tool supports Java versions through
OpenJDK 7.
Licensing:
The plug-in builds on the Eclipse JDT and PDE, through their public interfaces;
it does not modify or contribute to Eclipse itself.
The source for the plug-in is available at the
jmlspecs sourceforge project.
This version of the plug-in is offered without cost and without warranty of any kind.
Feedback that will
improve its usefulness is welcome.
This version of the plug-in is distributed under the
Eclipse Public License.
The copyright is retained by the primary author.
Future versions may use other licenses.
The underlying OpenJML tool is built on
OpenJDK
(OpenJDK is a trademark of Oracle).
OpenJDK and thus OpenJML is licensed under
GPL.
The plug-in adds the following functionality to Eclipse's Java Perspective:
- A menubar item labeled 'JML' with a number of submenu items that
invoke various tools and manage the environment.
- Toolbar items labeled with the JML yellow coffee cup icon that invokes the JML syntax and type checker,
with 'ESC' to invoke static checking, and with 'RAC to invoke runtime assertion compilation.
- Problem markers: a red, yellow, orange and blue disks with a 'J' on then for JML problems,
JML warnings, JML static checking (ESC) warnings, and JML informational messages, respectively.
These must be enabled in the Filters menu of the Problems view (they may be
disabled by default).
- Annotation preferences. On the General>Editors>TextEditors>Annotations
preference page are four new categories for the four new problem markers. This
preference page contains controls for determining whether and how editor annotations
are displayed in editors - e.g. as squigglies, in the overview ruler (on the right),
in the vertical ruler (on the left), and in what color.
- Context menu items in various views
and on Java editors that replicate some
of the above menu items for Java Projects, source
folders, packages, compilation
units, working sets, and individual classes and methods.
- The plug-in recognizes the standard JML file suffix (e.g. .jml);
this suffix is bound to the Java editor. JML annotations themselves, however, are
still treated as comments by the Java editor.
- A console page to which output from the JML operations is sent.
- An OpenJML preferences page
(under Window >> Preferences >> OpenJML).
- A JML builder that is visible (when the JML Nature is enabled)
in the Project Properties Builders page.
- A decoration visible in the package explorer (and other places)
on Java Projects with autochecking enabled. There is a toggle
named 'JML' to enable these decorations in the Label Decorations page of
the workbench preferences.
- Ability to generate javadoc documentation with JML material included.
- A new category of commands in the Workbench >> Keys page of the Eclipse
preferences. The category is named 'JML' and allows key bindings to be
defined for the various new menu actions.
- A Help document describing the JML plug-in functionality available
through the Help >> HelpContents menu (this document).
Besides the additions to the Eclipse UI, there is also a JML command-line tool
that can be executed outside Eclipse; the Eclipse UI simply drives the
command-line tool to do the type and static checking of JML specifications.
The plug-in is installed, updated, and uninstalled from Eclipse in the
standard way. The update site site containing the plug-in is
http://jmlspecs.sourceforge.net/openjml-updatesite.
Once installed, there are a few setup actions that the user needs to
do to avoid becoming confused later on. FIXME - these may now be moot.
- Enable the JML markers - By default new marker types
are not displayed in the 'Problems' View. To correct this, open
the 'Problems' View (typically in the lower right pane in a Java
Perspective), and then open the 'Filter' dialog using the toolbar
item or the menu on the right end of the Problems view's toolbar.
Make sure that the 'JML Warning' entry is checked.
- Be sure the JML Label Decorations are turned on in the
Label Decorations page of the Workbench preferences.
- Optionally define any desired key bindings for the various menu actions.
Use the JML category in the Keys page of the Workbench preferences to do this.
Add the key bindings to be effective in Windows or in Dialogs & Windows.
- Other preferences relevant to the JML plug-in may be set on the
JML preferences page. (The preferences page is
obtained from the Window >> Preferences menu item.)
There is one other important action that is taken care of automatically
but that the user should be aware of.
- JML specifications for the Java system and JML Model classes - To use
JML (or other JML-based tools) effectively, the tool needs to reference a
copy of the JML specifications for the Java system classes. A copy of these
is contained in the JML plug-in. When a project is enabled for
JML checking, a specification project (named JmlSpecs) is automatically
created and added to the workspace. This project contains a link to the
library of system specifications; the project is also added to the classpath
of the enabled project, so that the specifications are seen when individual
files are checked.
You may need to adjust the position of the specifications in the classpath.
If you have other versions of the system specifications (or other sets
of specifications for other libraries), you can conveniently add them
to your Java Projects by ...
Here are some aspects to be aware of in using the plug-in.
-
The JML functionality is provided by the OpenJML application.
-
Defining the Java Editor as the editor for the specification file suffixes
goes only part of the way towards convenient handling of specification files within
Eclipse. In particular, one difficulty is that editing specification files
will not trigger an
incremental compilation.
- Various features of the plug-in are enabled by default. If for some
reason they are or become disabled, the user may be confused that some
functionality is not visible. These features include
- JML problems in the problems view are visible only if "JML Problem" and "JML Static Check Problem"
are enabled in the currently active filter.
- JML decorations on project icons are visible only if "JML" is enabled
on the General >> Appearance >> Label Decorations preference page.
- JML annotations are visible within Java editors only if the appropriate
controls are set on the General >> Editors >> Text Editors >> Annotations
preference page. The colors of the annotations are also controlled here. The colors
of the 'J' icons are fixed.
- The OpenJML tool needs access to SMT solvers in order to do static checking.
These are set on the JML Preferences page or in the openjml.properties file.
- Key bindings to JML commands are set on the General >> Keys preference page.
No key bindings are set by default.
- Automatic type-checking of JML specifications is enabled by adding
the JML nature to a project using the provided menu action. In addition,
the JML Builder must be enabled in the project properties; the JML builder
is enabled by default when the JML Nature is added, but it is possible for
a user (or, possibly, other plug-ins) to disable it. Automatic type-checking
is not enabled by default, but is persistent. Only type-checking (not
static checking) is able to be automatic.
- JML type and static checking apply to the saved version of a
source file.
- Java refactorings (e.g. renaming) are currently not aware of JML information.
- Other tool options are set on the JML preference page.
-
The Eclipse framework operates on projects one by one. This is
required because attributes such as the relevant classpath for
compiling the project may differ from project to project. Hence
JML tools driven by Eclipse must also operate project by project; this is ordinarily
not a problem but can in some circumstances lead to slow or
undesirable results. This problem is avoided if everything that
can be compiled with a given classpath is contained in one project,
with one output bin directory,
possibly using multiple source folders.
-
Internal errors or unexpected exceptional situations are logged in
Eclipse's error log. The JML page of the Eclipse Console
may be used to report progress and general debugging information, if
that output is enabled in the JML preferences page.
This section describes how to accomplish a number of common actions.
Later sections provide a reference manual style enumeration of the plug-in's
functionality.
TBD
TBD
Type-checking JML specifications
TBD
Automatically type-checking specifications
TBD
Viewing the combined JML specifications of a class or method
TBD
Changing the source of Java library specifications
TBD
Changing the classpath used by the JML tools
TBD
Running static checks on Java source
TBD
Inspecting the result of static checking
TBD
Compiling and executing assertions at runtime
TBD
Creating key bindings for a JML action
TBD
Changing how problems appear in Java editors
TBD
Changing how JML tools operate (preferences)
TBD
The top menubar provides the following functionality. The toolbar
and the context menus replicate some of this functionality. The menubar
item is labeled 'JML'.
Each of the menu operations act on the currently selected set of objects
as appropriate for that operation.
If an editor is selected and active, the operation will apply to the
one Java compilation unit in that editor. If a WorkingSet is selected, it will
apply to the Java Projects in that Working Set.
In Eclipse's Package Explorer view, multiple items may
be selected. The operations will act appropriately on
each selected Java Project, container or file.
Selecting a container item will cause
the relevant operation to be performed on all the items within the
container. Currently, selecting a Java element within a file (e.g. a method)
does not result in any operation, though some appropriate action may be
implemented in the future.
Type Checking JML
This operation type-checks the JML in each selected item or its contents.
The operation can be initiated from the menu item or by the the yellow coffee
cup toolbar item or from various context menus.
Any JML syntax or parsing errors are presented as problem markers.
How problems are identified depends on the preferences set in
General>Editors>Text Editors>Annotations. These items can be set or
their colors changed:
- showing problems by underlining with squigglies
- showing problems by highlighting
- showing problems by an icon in the left (vertical) ruler
- showing problems by marks in the right (overview) ruler
In addition problems are shown in the Problems View, if enabled by the content
selection for the Problems View.
If
problems are enabled in the Problems View, then details of the problem
are shown in the Problems View. This menu item performs
a check whether or not the project is enabled for automatic checking.
It operates on the saved version of the source file,
not the current edited but unsaved version.
A JML Check operation needs to parse files other than those selected
if they are referenced by the selected files. Thus errors may be
detected (and markers produced) in files other than those selected.
Prior to executing the checking operation, all markers are cleared
from the selected files, so that a fresh set of error reports is
available. However, non-selected files are not cleared, which may
result in multiple markers being produced for problems in other files.
Also, if the error is subsequently corrected but the file with the marker is
not selected when the JML Checker is run again, the marker will not be
cleared even though the problem is no longer present. An occasional
type-check of an entire project is a quick way to solve this problem.
Alternately all problem JML markers can be cleared, so they are all created
afreash.
Static Checking JML
The Static Check operation is available as a menu item, toolbar item, and in
the context menus of various Java elements. It checks for each method in the
selected set of Java elements whether the method's implementation is consistent
with its specification. Warnings about possible inconsistencies are displayed
as JML Static Check Problems, in the conventional way Eclipse problems are
displayed. The icon in the left ruler is an orange disc with a J.
Delete JML Markers
The Delete Markers operation removes all problem markers from any selected
files or
containers.
Enable JML auto checking
Enabling the JML
autochecker will install the JML Nature on the project and enable the
automatic builder. Then after any compilation (even an incremental compilation),
the JML checker will be run on any newly saved compilation units of the project.
The checker will be run on the entire project immediately upon enabling the
automatic builder. This menu item is also available on WorkingSets in the
Package Navigator; when activated, it applies to all of the Java projects in the
working set. The auto checker is enabled or disabled only on Java Projects, not
on components of projects.
Disable JML auto checking
This menu action disables the JML automatic checking for a project.
The menu item is also available on WorkingSets, in which case it applies to
all of the Java Projects in the working set.
The auto checker is enabled or disabled only on Java Projects, not
on components of projects.
Note that you can also disable automatic checking on the Builders page of the
Project >> Properties menu item, without removing the JML Nature of
the project.
This action is discouraged.
Show Proof Information
TBD
Show Specs
TBD
Add to Specs Path
TBD
Remove from Specs Path
TBD
Edit the Specs Path
TBD
Show the Classpath
TBD
Generate JML doc
TBD
Show counterexample value
TBD
Enable for RAC
TBD
Compile for RAC
TBD
Disable for RAC
TBD
Delete RAC class files
TBD
Toolbar
The tool bar contains three additions:
- A yellow coffee cup icon: this button performs JML type-checking on
selected files,
the same operation as the JML type-check menu action.
- ESC: this button performs static checking of selected files, the
same operation as the Static Check menu item
- RAC: this button performs assertion compiling, the same operation as
the RAC menu item
Context menus
There are JML specific items added to the context menus in various views such
as the Package Explorer, Navigator and Outline views.
Context menus are obtained by right-clicking (Control+Click in MacOS) on the
desired item.
In each case the functionality is the same as for the corresponding menubar item,
but the operation applies only to the item right-clicked upon. Multiple items
can be selected (using shift-click or control-click) and operated
on at once using the context menu, but the context menu item will be disabled
if an item is selected to which the menu item does not apply
(even in a group of other items to which the menu item does apply).
| Enabled for: |
Working sets |
Java Projects |
Folders and packages |
Files |
Classes |
Methods |
Fields |
| Type check |
X |
X |
X |
X |
F |
- |
- |
| Static check JML |
X |
X |
X |
X |
? |
? |
? |
| Enable/Disable JML Auto checking |
X |
X |
- |
- |
- |
- |
- |
| Clear Markers |
X |
X |
X |
X |
F |
- |
- |
- X = action applies to the element or its contents
- P = action applies to the containing project
- F = action applies to the containing file
- M = action applies to the containing method
- ? = not working correctly
- - = action is not enabled
FIXME - complete the table
JML preferences
The plug-in provides a new preference page under Window>>Preferences; it is
contained under the 'JML' heading.
All the items in the JML preferences page are global to all
Java projects.
TBD - FIXME - This needs rewriting.
Other Features
JML Problem Markers
The plug-in defines two new types of Problem marker that is used to indicate
syntax errors or warnings about potential specification violations
that the JML tool finds. The marker icon is a
white 'J' superimposed on a dot. The icon is shown in the ruler along the
left edge of Java editors at the line where a problem is identified. Tooltip
information, shown when the mouse pointer remains steady over the icon for a short
period of time, gives details of the problem.
- red dot - JML syntax error
- orange dot - Static checking warning
- yellow dot - JML syntax warning
- blue dot - JML informational message
The
details of the problem are also shown in the Problems View. Note that the Problems
View has a filter that chooses which types of problems are to be shown. The
JML problem type is NOT shown by default and must be enabled in the
filters menu of the Problems View. (The filters menu is found by selecting either
the Filters icon or the down-arrow Menu icon in the upper right corner of the
Problems View). [ FIXME - is it still true that the markers are not shown by defzault?]
JML Console
The Eclipse Console View is available to plug-ins to show textual output from
plug-in tools. The Console has a number of panes. The JML plug-in adds
a new pane, called 'JML', to which output from the JML plug-in or
tool is sent. The Console view generally automatically switches to the pane
with recent output, but on some occasions the user may have to choose the
pane manually to see the JML output. (The Console can also be pinned to
disable automatic switching.)
Context Menus
The context menu in the Package Navigator (obtained with a right mouse press over
an item in the Package Navigator tree hierarchy) has menu options pertinent
to the context in which the menu is invoked. These actions are equivalent
to those in the menubar.
JML Automatic Builder
When JML is enabled for a project
(e.g. by the JML >> Setup >> Enable JML menu item), then
a new Incremental Builder becomes available on the Project's
Builders Properties page. Once present, the builders can be
enabled and disabled on the Builders page.
When the 'JML AutoCheck' Builder is enabled, then whenever compilation
takes place within a project, all files in that project are JML-type-checked
after being compiled.
Success or failure of this checking is shown by the presence of
JML markers
in each file, just as errors from the Java compiler are show by Java Problem markers.
Enabling auto checking will cause Eclipse to immediately run a compilation
cycle on that project.
Note that changing the options on the JML preferences page does not
constitute changing the file and will not provoke an incremental
recompilation (and JML rechecking) of the files. Instead, if you
change the JML options (when you have auto checking enabled), you should
do a clean rebuild of the files (or a gratuitous edit and save within them).
Be sure to save any edited files, or have 'Save automatically before build'
enabled on the Workbench Preferences page (from the Window>>Preferences menu item).
JML Label Decorations
The plug-in adds a new label decoration to the Eclipse framework.
Label Decorators can be
enabled or disabled on the Workbench>>Label Decorations page of the
workbench Preferences. When enabled here, a decoration may be shown on
icons in the Package Explorer view.
The decoration is a miniscule version of the JML logo (a mostly yellow coffee cup);
it appears as an Upper Right
overlay for Java Projects that have JML enabled.
(It lies on top of the
blue J indicating a Java Project.)
JML Key Bindings
The 'Keys' page of the Workbench preferences allows the user to
associate key bindings with any
command. There is a JML category of commands.
No key bindings are defined by default, but the
user may choose to add some. Make sure they are enabled for 'Windows'
or 'Dialogs and Windows'.
JML Help
Help information (this document) is available through the Help menu.
Select the Help menu item on the menubar and the 'Help Contents'
sub-menu item. One of the help topics shown is 'JML'. Selecting
that topic will bring up this JML Help document.
In addition all the various toolbar and dialog box controls have tool tip
information that gives a bit more explanation of the purpose of the item.
Version history
Getting Started Tutorial
--- not written yet -- (FIXME)
Notes for Developers
--- not written yet -- (FIXME)
Problems to fix and features to add
This section summarizes in bullet form
outstanding issues and future would-be-nice features.
--- not written yet -- (FIXME)
Major nuisances
- Need to document here the command-line tool
- JML problems are not enabled by default
Minor nuisances
Would be nice
Uncategorized issues