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: 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:

Using JACK

The integration of JACK in the Eclipse IDE consists in:

How it works

From an annotated Java file to lemmas: