To check whether java is available and the command line, press Win+R, enter cmd and press enter. Type java -version. If you get the response that the command is not available, add it to the path:

set PATH=%PATH%;"C:\Program Files (x86)\Java\jre6\bin"

where the exact installation path of java may differ. Check whether the path is correct now by the command echo %PATH% and if java -version gives a response now.

Download the OpenJML package here or, since tar.gz might not be handled, we have a local copy in ZIP format here. In this tutorial we assume that you extract this file to the same folder as where JMLTest.java resides, if not, you need to change the paths in the following instructions accordingly.

Navigate the windows commands prompt to the folder with the extracted jars and the JMLTest.java. To check the JML annotation run:

java -Xbootclasspath/p:openjml.jar -jar openjml.jar -noInternalSpecs JMLTest.java

The tool will find one error that we left in the file on purpose, fix it, save the file, and run the same command again to see that everything is correct now. Note that if you forget to include the -noInternalSpecs flag you will get a bunch of warnings related to the internal JML specification in OpenJML.

Download the OpenJML command line toolset:

wget http://jmlspecs.sourceforge.net/openjml.tar.gz

Extract:

tar xzvf openjml.tar.gz

Of main importance are the .jar files. The user guide might be of interest as well, however if you open it you will find many sections are still "to be added later". Now, assuming that you have the JMLTest.java file in this same directory, we can check the JML syntax in this file:

java -Xbootclasspath/p:openjml.jar -jar openjml.jar -noInternalSpecs JMLTest.java

The tool will find one error that we left in the file on purpose, fix it, save the file, and run the same command again to see that everything is correct now. Note that if you forget to include the -noInternalSpecs flag you will get a bunch of warnings related to the internal JML specification in OpenJML.

java -Xbootclasspath/p:openjml.jar -jar openjml.jar -rac -noInternalSpecs -source 1.6 -target 1.6 JMLTest.java

bash-3.2$ java -classpath ':*' JMLTest 12
JMLTest.java:5: JML invariant is false
JMLTest.java:5: JML invariant is false
Balance: 13
JMLTest.java:5: JML invariant is false
Done
bash-3.2$ java -classpath ':*' JMLTest -3
JMLTest.java:10: JML precondition is false
Balance: -2
Done

sudo update-alternatives --config java

Install the Eclipse plugin (requires Eclipse 3.6 or later). Go to the menu Help -> Install New Software... Click on the button Add and enter the following information:

Name:     openjml  
Location: http://jmlspecs.sourceforge.net/openjml-updatesite

Select the OpenJML package, click Next and accept the license agreements presented (if you choose to). After installation, Eclipse needs to be restarted. If everything went okey, you should now find the following buttons somewhere in your main menu bar:

Clicking the coffeecup will make OpenJML check your specification and mark red what is incorrect (you do need to manually save the file before). The ESC button can be used for static checking, but we will not cover that now. The RAC button compiles the programs and inserts Run-time Assertion Checks based on your JML annotation. Try the JMLTest.java file mentioned on the top of this page. Change the main function to not use the argument from the user but supply in directly in the code if you like, and see if you can break the invariants (and whether the RAC detects them). Note that everytime you save you have to press RAC first and Run after that, otherwise the 'standard' compiler (without assertions) is used.

If the OpenJML icons do not appear, you are most likely not running Eclipse in Java 1.7.

We assume that you have the java command available at the command line. To check this, press Win+R, enter cmd and press enter. Type java -version to see if and which version of java is there. If you know java is installed but it does not show up on the command line, you can add it to the path as follows:

set PATH=%PATH%;"C:\Program Files\Java\jdk1.7.0_01\bin"

where you should of course use the right path to your installation. For syntax checking only a jre (not compiler) is also sufficient. Check whether the path is correct now by the command echo %PATH% and if java -version gives a response now.

Download the OpenJML package here and extract it to the same location as JMLTest.java (if you place it in a different directory you have to update the paths below accordingly). Download 7-zip if your current installation does not support this type of compression.

Navigate the windows commands prompt to the folder with the extracted jars and the JMLTest.java. To check the JML annotation run:

java -Xbootclasspath/p:openjml.jar -jar openjml.jar -noInternalSpecs JMLTest.java

The tool will find one error that we left in the file on purpose, fix it, save the file, and run the same command again to see that everything is correct now. Note that if you forget to include the -noInternalSpecs flag you will get a bunch of warnings related to the internal JML specification in OpenJML.

java -jar openjml.jar -rac -noInternalSpecs JMLTest.java

C:\Users\Bart\Desktop\openjml>java -classpath .;* JMLTest -1
JMLTest.java:9: JML precondition is false
Balance: -1
Done

C:\Users\Bart\Desktop\openjml>java -classpath .;* JMLTest 14
JMLTest.java:4: JML invariant is false
JMLTest.java:4: JML invariant is false
Balance: 14
JMLTest.java:4: JML invariant is false
Done

Install the Eclipse plugin (requires Eclipse 3.6 or later). Go to the menu Help -> Install New Software... Click on the button Add and enter the following information:

Name:     openjml  
Location: http://jmlspecs.sourceforge.net/openjml-updatesite

Select the OpenJML package, click Next and accept the license agreements presented (if you choose to). After installation, Eclipse needs to be restarted. If everything went okey, you should now find the following buttons somewhere in your main menu bar:

Clicking the coffeecup will make OpenJML check your specification and mark red what is incorrect (you do need to manually save the file before). The ESC button can be used for static checking, but we will not cover that now. The RAC button compiles the programs and inserts Run-time Assertion Checks based on your JML annotation. Try the JMLTest.java file mentioned on the top of this page. Change the main function to not use the argument from the user but supply in directly in the code if you like, and see if you can break the invariants (and whether the RAC detects them). Note that everytime you save you have to press RAC first and Run after that, otherwise the 'standard' compiler (without assertions) is used.

If the OpenJML icons do not appear, you are most likely not running Eclipse in Java 1.7.

Note: if you get errors saying that packages don't exist, eclipse probably has the problem that is cannot parse the path (linux vs windows issue) correctly because of the whitespace in "Program Files". The easiest options is to add C:\Program Files\eclipse\plugins\org.jmlspecs.OpenJMLUI_0.2.5\jmlruntime.jar (or a similar path) to your project's build path. You will still get the failure messages but at least the tool works :-)

If you get the message "Unsupported major.minor version 51.0" this means that the version of the compiler you used differs from the version of the virtual machine you are running. Fix this in your OS / IDE.