You can download the Java sources for the exercises here.

You can download the solutions for the exercises here.

Exercise 1

A bank offers its customers certain services at the bank's numerous automated service terminals. Using the card and a PIN, the customer can check the balance of his account, he can withdraw cash and he can initiate a mailing of a printed account statement. If a wrong PIN is given 3 times in a row then the card is confiscated by the service terminal. A withdrawal of cash may not be larger than the current balance of the account and in any case may not exceed 1000 euros per day. This can obviously be enforced if the respective ATM is online. If an ATM cannot establish a connection to the bank, an offline cash withdrawal without check of the balance is made. The sum of all offline withdrawals until the balance can be checked and adjusted may never exceed 1000 euros, regardless of the number of days. There may be more than one card for each account. Issue of cards and opening of accounts is done with the central host. The cards themselves contain no software, but are basically data containers. It is possible to receive a written account statement for free once a month.

Javadoc is available here

Adjust the settings in KeY under Proof Search Strategy as following:

• Arithmetic Treatment - DefOps
• Quantifier Treatment - No Splitting with Progs
• Query Treatment - Expand

1. In the file ATM.java provide the implementation for insertCard/ enterPIN according to the specification provided
2. In the file ATM.java provide a specification for getAccount(int accountNumber). Hint: Take into account the invariants from CentralHost.java.
3. In the file PermanentAccount.java provide a specification for dailyLimitIsImportant.
4. In the file ATM.java check that the methods confiscateCard and accountBalance fulfill their postcondition and preserve the class invariants. Explain the proof obligations that are generated !
5. Check that the specifications provided for 2 and 3 preserve the class invariants and ensure the postconditions. Hint: You might need to consider invariants from other classes also!

Exercise 2

What does the following method do, assuming that x is a positive integer ?

public int x;

public int method() {
   int  y = x;
   int  z = 0;	
       while (y > 0) {
                      z = z + x;
                      y = y - 1;
                      }
 
       return z;
    }

1. Write JML specifications for method and invariants for the class.
2. Prove partial correctness for method by providing a loop invariant.
3. Is total correctness possible to prove ? Justify !

Exercise 3

What does the following method do, assuming that x is a positive integer and y is a strictly positive integer?

 
public int x;
public int y;
    

public int method() {
	int  x1 = x, q = 0;

        while (x1 >= y) {
                       x1 = x1 - y;
                       q = q + 1;
                       }

       return q;
    }

1. Write JML specifications for method and invariants for the class.
2. Prove partial correctness for method by providing a loop invariant.
3. Is total correctness possible to prove ? Justify !

Exercise 4

Exercise 5

1. Specify the normal and exceptional behavior of method activateLicense of class Person.
2. Verify that both contracts ensure their respective postcondition.
3. Verify that the method activateLicense preserves the invariants of class Person.