CSSE 373 Formal Methods in Specification and Design

Installing the Mobius Program Verification Environment

What is it?

The Mobius Program Verification Environment (PVE) is a custom Eclipse configuration that includes tools for (surprise) program verification. These tools include:

• ESC/Java2 — the Extended Static Checker for Java, a tool that reads program specifications written in the Java Modeling Language (JML) and uses a custom automated theorem prover to check that the specification hold
• RAC — the Run-time Assertion Checking compiler, a tool that converts JML annotations to run-time checks that detect specification violations while the annotated program is running
• JML Folding Editor, an editor extension that is supposed to help users edit JML-annotated programs

Mobius PVE includes a variety of other tools as described on the Mobius Wiki. Mobius PVE is open source under a variety of licenses. (It's really a compendium of several open source projects in a handy wrapper.)

Because the Mobius PVE is a complete Eclipse installation, we can use it without screwing up existing Eclipse installations. The cost, of course, is more hard drive space used.

Downloading Mobius PVE

On Campus

From on campus, you can save bandwidth costs by downloading one of the following local zip archives:

• Linux
• Mac OS X
• Windows

Off Campus

From off campus, you can download the same zip files directly from the Mobius PVE downloads page. (We’re using the Delta release. The Mobius team is working on posting the Epsilon release this week, but it won’t be ready in time.)

Configuring

Extracting the program

Just unzip the downloaded zip file and put the resulting folder whereever you keep such things on your machine.

Configuring a Workspace

Follow these steps to configure a new workspace for working with the Mobius PVE:

1. Launch the Eclipse application inside the extract Mobius folder.
2. Create a new workspace like you normally would in Eclipse.
3. Tell ESC/Java2 to use the built-in version of the automated theorem prover as follows:
   1. Open Eclipse Preferences.
   2. Navigate to Java → ESC/Java2
   3. Make sure the checkbox for Use Internal Version is checked.
   4. Apply and close the Eclipse Preferences.

Using ESC/Java2

Follow these steps to create a new Java project that uses ESC/Java2 for checking:

1. Create a new Java project in the usual way.
2. Click on the project in the Package Explorer view.
3. In the Eclipse menu bar, choose JML → Setup → Enable ESC/Java Nature.
4. You should see a new jmlspecs project appear in the Project Explorer view. You shouldn’t make any changes to that project. It is created there by ESC/Java2 and contains JML specifications for important parts of the Java API.
5. You’ll probably get (in the Console view) an error “Failed to install JML specification”. You can ignore this; it’s just a timing problem on the first run of the checker.
6. Now you can write Java code as you normally would in Eclipse. As you do so you'll find:
   • ESC/Java2 detects possible null pointer dereferences. If it indicates that a field access or method call on a parameter—say x—might involve a null pointer, you can add a pre-condition that says x != null. Now the checker will be happy with the field access or method call, but will check that you never pass null as the value for parameter x.
   • ESC/Java2 detects possible violations of JML pre-conditions, post-conditions, and class invariants. It places an error marker in the side bar. Hover the mouse over the side bar to see a description of the problem.
   • ESC/Java2 does not support Java 5 generics. An on-going NSF grant is working to remedy this.