Eclipse Mars 使用 OpenJML

强力软件

Installation

1. You must have Eclipse Kepler or Luna (Since Mars is newer, I guess it should work).
2. Select menu Help >> Install New Software, add http://jmlspecs.sourceforge.net/openjml-updatesite.
3. Install OpenJML plugin.
4. Restart Eclipse.

A few more things you need to do:

• In Project Explorer View, select your project and Enable JML in right mouse menu.
• On the OpenJML Solvers preference page, select a default solver and enter the path to the solver executable.
• On the OpenJML preference page, select the 'Skip Purity Check' option.

NOTE: You might encounter "Errors running builder 'JML Builder' on project" while enabling JML. This problem is caused by the layout of you project, you should not select Use project folder as root for src and cls.

NOTE: The OpenJML preference page is in Window -> Preferences -> OpenJML.

NOTE: Since NO Fucking SMT tool for LINUX

Run with Command line

Type-checking

java -jar $INSTALL/openjml.jar -no-purityCheck A.java

Static checking

java -jar $INSTALL/openjml.jar \
    -esc -prover z3_4_3 -exec ${smt-exec} \
    -no-purityCheck B.java

You should replace z3_4_3 with yices2 if using yices2.

Runtime assertion checking

java -jar $INSTALL/openjml.jar -rac -noPurityCheck B.java