Overview

• About
• People
• Related Projects
• Download
• Sourceforge

Documentation

• Installation Notes
• ESC/Java2 Plugin
• About
• Installation   Notes
• Project Notes

Support

• Forums
• Bugs/Feature Requests
• Mailing Lists

The plug-in is installed from a standard Eclipse update site as follows.

• Start Eclipse.
• Open the dialog at Help >> Software Updates >> Find and Install.
• Choose "Search for new features to install" and "Next>".
• Select "New Remote Site". Fill in the dialog with the name "Esc/Java2" and the URL http://sort.ucd.ie/www/escjava-eclipse/updates, and press "OK".
• Select "Esc/Java2" in the list of sites to search and press "Next>".
• If all is well, the available versions of the plug-in will be displayed; select the most recent Esc/Java2 version and press "Next>".
• Read and accept the license terms, and press "Next>".
• Choose the local installation site into which you want to install the plug-in (or add a new one for experimentation); then press 'Finish'. You will likely be asked to restart the workspace, which you should do, otherwise the menu items may not appear.
• The plug-in will be available from any newly opened workspace from this installation site.
• The plug-in can be disabled or uninstalled using Help >> Software Updates >> Manage Configuration.

The source code for the plug-in is available, in accord with the Eclipse Common Public License.

If you simply want to update a previous installation of ESC/Java2, then do the following:

• Open an Eclipse workspace and choose Help >> Software Updates >> Find and Install.
• Choose "Search for updates..." and "Next>"
• Select the feature version to install and "Next>"
• Read and accept the license terms, and press "Next>".
• Choose the local installation site into which you want to install the plug-in (or add a new one for experimentation); then press 'Finish'. You will likely be asked to restart the workspace, which you should do.
• The updated plug-in will be available from any newly opened workspace from this installation site.

In order to uninstall the plugin, do the following:

• Choose Help >> Software Updates >> Manage Configuration
• Click the + symbol by the install location from which you wish to uninstall the plugin
• Choose the Esc/Java2 feature from the list of installed features
• Select Uninstall in the right hand panel
• Confirm the Uninstall and restart the workbench

Once installed, there are a few setup actions that the user needs to do to avoid becoming confused later on.

• Enable the ESC/Java2 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 'ESC/Java2 Warning' entry is checked.
• Define file associations for specification file suffixes - The Java perspective does not treat specification files as first-class Java files, but it is at least helpful to be able to use the Java editor on these files. So choose Window >> Preferences and then Workbench >> File Associations. In turn, add the entries '*.refines-java', '*.refines-spec', '*.refines-jml', '*.spec' and '*.jml' as new file types in the upper panel and add the Java Editor as the default editor for each of these suffixes in the lower panel.
• Be sure the ESC/Java2 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 ESC/Java2 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 Esc/Java2 plug-in may be set on the Esc/Java2 preferences page under the Java category. (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 ESC/Java2 (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 ESC/Java2 plug-in. When a project is enabled for ESC/Java2 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 ...

General comments

Here are some aspects to be aware of in using the plug-in.

• The ESC/Java2 functionality is provided by integrating the Eclipse extension capabilities directly with the ESC/Java2 tool. ESC/Java2 is a standalone tool with its own parser and compiler for Java. Consequently, when ESC/Java2 operations are run within Eclipse, the Java files are parsed over again. This can result in duplicate error messages (as well as slower than ideal performance).
• ESC/Java2 operates on files as they exist in the file system. Thus editors within Eclipse must be saved if ESC/Java2 is to see any newly edited material.
• 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.
• 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 ESC/Java2 (and JML tools) 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.
• ESC/Java2 was not designed for interactive use. Consequently operations cannot be canceled and restarted readily, so the user may experience a slow response to cancellation. The tool also is not designed to support incremental analysis.
• Internal errors or unexpected exceptional situations are logged in Eclipse's error log. The ESC/Java2 page of the Eclipse Console may be used to report progress and general debugging information, if that output is enabled in the ESC/Java2 preferences page.