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:

    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.