Installation Notes
- 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 Error' 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 JML Label Decorations on 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.
- The jml-release.jar library - In order to compile and run a program
in which runtime assertion checks are desired, a project must have the
jml runtime library classes on its classpath. These classes are available
as part of the plugin. The library is automatically placed on the
classpath for a project when the JML Nature is enabled for the project.
If it fails to happen, or you wish to use a different version of the runtime
library, you will need to manually complete the following steps. You
may also wish to adjust the position of the library in the classpath.
- Select the project to which the library is to be added and open the project properties page (via the Project->Properties menu item).
- Choose the 'Java Build Path' page and its 'Libraries' tab.
- Press 'External Jars', navigate to the location of the jml-release.jar library in your file system, select it, and press 'Open'.
- Press 'OK'.
- If necessary, adjust the position of the library in the classpath on the 'Order and Export' tab.
- JML specifications for the Java system and JML Model classes - To use
the JML Checker (or other tools) effectively, the tool needs to reference a
copy of the JML specifications for the Java system classes. These are contained
in the library jmlspecs.jar. However, the JML tools cannot access them from
a JAR file, but need to access them from a source code hierarchy. These also
are part of the plugin and are automatically inserted into a project
when the tools are run.
The JML specifications will appear as a new, automatically added, Java project named 'JmlSpecs'. JML enabled projects will have this project added to their classpaths; you can easily enable and disable the use of the specs in a given project by toggling the JmlSpecs project on the 'Projects' tab of the Java Build Path' page of the project's properties dialog.
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 using the JML->Setup->Link in Specs Library menu item. This allows you the choice of adding a set of specifications as either a stand-alone project or as a new source folder in a specific project. Using a standalone project makes it easier to share the specs among multiple projects and to toggle the use of the specs on and off within a given project.
Note that if you want to delete the created source folder, you must first remove it from the project's classpath, and then you can simply delete the folder.
Technical notes: The specifications are included by creating a source folder that is linked to the file system location of the specification files. The specs are also 'excluded' so that the Java compiler does not attempt to compile them (even if they are in Java files).