ATM_Example_JML
This directory contains the files ATM.java, BankCard.java  and
CentralHost.java. The Java code plus JML specification from 
Figure 5.14 on page 277 is part of the ATM.java file. 

To run it start the KeY prover ( call key/bin/runProver) and load the
directory. Proceed by using the JML browser as explained on pages 445ff.
Make sure that the Proof Search Strategy activates Java DL.
The settings for Loop treatment, Method treatment, Query treatment
do not matter. Arithmetic treatment should be basic.
All proof will complete automatically without use interaction.

======================================================================
While-Example_JML
This directory contains the file with the Java+JML example from 
Section 5.3.6 on page 289. The example only considers loop invariants. 
The file WhileDemo.java contains a method that makes use of this while loope 
plus JML specification.

To run it start the KeY prover ( call key/bin/runProver) and load the
directory. Proceed by using the JML browser as explained on pages 445ff.
Make sure that the Proof Search Strategy activates Java DL and  Loop treatment
is set to "Invariant".
The proof proceed automatically with to open goals remaining.  These can
be closed calling on of the decision procedures "simplify" or "Yices".
======================================================================
ATM_Example_OCL
In order to run this example you need Borland-Together 6.2 (unfortunately later
versions do not work). You have to buy a licence for this package.

This directory contains the OCL specification from Figure 5.2 from
page 250 and the program from Figure 5.3 on page 253.
The example contains slightly more details than the book example.
The method pinIsCorrect( pin ) from the class BankCardm which is not
shown in the book, e.g. checks wether the card is invalid. This necessitates
an additional precondition for the contract for enterPin to be provable.

The run the example load the project ATM.tpr into Together. Select in the
class diagram frame method enterPin in class ATM. The right mouse button will
produce a pull-down menue. Select at its very lower end the KeY submenue.
From there select Vertical Proof Obligations and further EnsuresPost(total).
The KeY prover window will show up. Make sure that you use the correct
Proof Search Strategy: activate Java DL, Query treatment should be expand,
the rest does not matter for this example.
Automatic symbolicall executtion of the program will terminate with some
ten goals open. This can be automatically closed by the simplify or Yices
decision procedure.