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 perspective containing three views:
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.