OpenJML install guide

Install guide for OpenJML.md

Install guide for OpenJML

If you have any problem, send an email to pierre.beaujean@unamur.be, find me on Discord or IRL in the lecture room, I'll be happy to help ;)

Preamble

Whatever your choice, OpenJML only runs with Java <= 8. Thus, you need to install this version of Java.

On ubuntu, you may do the following:

sudo apt install openjdk-8-jre openjdk-8-jdk

To set, at any time, the default version of Java (if you need Java 11 for something else), run

sudo update-alternatives --config java

There should be similar command for other flavor of Linux, but this covers Debian-based one.

For Windows and macOS go to https://www.java.com/en/download/manual.jsp, download and install Java 8.

Method 1: command line tool

1. Download the latest release at https://github.com/OpenJML/OpenJML/releases (the download link on the website seems broken) ;
2. Extract it in any folder. Inside the archive, there is a folder called openjml-0.x.y-zzzz (where x and y are version, and zzzz is the date of the release). I will refer to the path to that folder as <OpenJML>.
3. To actually run OpenJML on a Java file, the command line is java -jar <OpenJML>/openjml.jar -esc /path/to/your/java/class.java.

For example, on the following class

class Test {
    //@ ensures \result > 0;
    public int test() {
        return 0;
    }
}

The output should be something like

./Documents/test.java:4: warning: The prover cannot establish an assertion (Postcondition: ./Documents/test.java:2: ) in method test
        return 0;
        ^
./Documents/test.java:2: warning: Associated declaration: ./Documents/test.java:4: 
    //@ ensures \result > 0;
        ^
2 warnings

which clearly states that the code cannot fullfill the post-condition. Switching return 0 for return 1, and running the check again, there should be no output: everything is OK.

Method 2: run inside IntelliJ IDEA

IntelliJ IDEA is an alternative for Eclipse. Although pretty nice for lots of stuffs, it does not provide a plugin in its latest versions (because it is a plugin made by an independant person, which does not follow the update of IDEA), and the creators of OpenJML seems to only support Eclipse. Therefore, I (Pierre) take the responsability for providing this plugin for the latest (2019.2.*) version.

Use the right Java version

First of all, please be sure that Java 8 is installed (see above). Then, set the project JDK to this version of Java by going into File > Project Settings. In the "Project" tab, set the project SDK to 1.8:

Install the plugin

Then, download the plugin (ZIP file below). To install it, go to File > Settings, and in the "Plugins" tab, select the wheel and use "Install Plugin from Disk":

You will need to restart Idea.

Setup stuff(s)

Before using the plugin, you need to configure it. Go to File > Settings and select the "OpenJML" tab:

If you didn't download OpenJML, now is a good time, through the "Donwload" button at the bottom. Clicking this button first require to set a destination directory (I strongly advise to create a directory for the destination, because the IDE will not create it), then download the archive, and unzip it in the destination you selected. It finally sets the path to OpenJML accordingly. Otherwise, you can set the path to the <OpenJML> directory by yourself by cliking the directory icon at the right of the corresponding input.

Then, you need to set a solver. Update the list with the "load" button. You must use a Z3 solver, otherwise this will result in (strange) errors. I advise you to select the latest one (z3-4.7.1).

Finally, check the "Add Sourcepath" and "Add Classpath" checkboxs. Otherwise, inheritance will not work.

Use

To use the plugin, simply go to Tools > Run OpenJML, or use Ctrl + Shift + O (only for the community version). The output should be located at the bottom of the window:

And voilà ;-)

Method 3: Eclipse

Follow those instructions (not tested).

openjmlplugin-1.0.4.zip