The JACK plugin

Introduction

The JACK converter converts a JML file to lemmas allowing proving properties on Java program. Developers add the properties in a Java file as special annotations. These annotations are written using the JML syntax.

Limitations

This section lists the main limitations of JACK.
Java limitations:

Floating point: JACK does not consider floating point values and computations.
Multithreading: JACK will only allow reasoning on a single thread.

JML limitations:
JACK accepts a subset of the JML language.

Installation Procedure

In this chapter, we describe the different steps necessary to install JACK.
What is necessary
To install JACK, you need:

to have already installed eclipse;
to update eclipse with the plugin;
to download the library files

Using JACK

The integration of JACK in the Eclipse IDE consists in:

A Preference page at workspace level,
A Properties page at project level,
A submenu in the contextual menu at Java source file level that allows to
- to generate proof obligations
- to edit the proof obligations
- to display metrics
- to prove the lemmas
Buttons
Some views:
- A proof task view
- A metrics view
A perspective containing three views:
- A case explorer
- A source viewer
- A lemma viewer

How it works

From an annotated Java file to lemmas:

the file is parsed and an internal representation is builded;
some other files are recursively loaded and parsed in order to link the loaded classes using the JML path;
all the declarations of the loaded files are linked and the JML clauses are type checked;
the bodies of the main file are linked and the JML clauses are type cheked and translated into formulas;
the proof obligations concerning the static initialization and all constructors and methods are constructed;
a weakest precondition calculus is applied on the calculated proof obligations resulting in lemma;
obvious lemmas are discharged;
the lemmas are saved into a jpo file.