First step with JACK

Configurate your general settings

In Window > Preferences > Jack,

set whether you want to generate obvious proof obligations (Obvious goals are those where the weakest precondition generation reduces to x ==x).

select in which formats the generated proof obligations should be displayed (current options: Java, B, Simplify and Coq)

select to use Simplify as obvious prover

Configurate the properties of your project

In Package Explorer, select project name. Click on right button and Properties > Jack. In this menu:

set your search paths for JML, e.g. the path where the annotated API can be found; the first usual error you may encountered with JACK is a link error due to the fact that it cannot find the default API;
generate an image; and
set defaults for the JML specification, i.e. if a certain clause does not occur in a method specification, what should be its default. One can set defaults for the requires, modifies, ensures and exsures clause

How to generate proof obligations and view them

Starting up Eclipse, open the Java perspective. In the package explorer, select an (annotated) Java file.
To generate proof obligations, use right mouse button and click Jack > compile
To view the generated proof obligations: Jack > edit
To prove them: Jack > prove

Short cut: the icons c, p and e in the top tool bar.

Settings for the Jack view

Once the Jack view has been opened Jack > edit, one can set options concerning the displaying of proof obligations.

When clicking on the arrow symbol on the top of the goal browser, one can select which goals should be displayed (only unproven, all goals, or only proven goals). One can also set when methods/cases should occur in the goal browser and finally one can select only goals of a certain type to be displayed.

When clicking on the arrow symbol on the bar between the file and the goal/hypothesis display, one can select which hypotheses should be displayed. By default, all hypotheses are shown, but one can select only a particular kinds of hypotheses to be visible.