Annotate the classes BankAccount and Person with invariants and 
preconditions. Start with BankAccount, then do Person.

You must establish the JML assertions already given in the code.

Also specify assignable clauses for each method.


You may notice that ESC/Java is more strict about signals clauses
than java is. In Java you can omit throws clauses for
Runtime exceptions, for ESC/Java you can't.

Some exercises:

1) Experiment with the use of the datagroup "objectState"
   to keep assignable specifications readable.  To do this, 
   declare that some field x belongs to the objectState by
        private int x; //@ in objectState;
   or, for arrays, by
        private int[] x; //@ in objectState;
        //@ maps x[*] \into objectState;
   to include both the array and its contents in objectState.

2) For the method debit in BankAccount.java, specify that the 
   balance won't change if this method throws a DebitException,
   using a signals clause.

3) For the method transfer in BankAccount.java, try to establish
   the postcondition
     //@ ensures balance == \old(balance) - amount;

   Coming up with the right precondition for this is tricky.
   (Hint: think about potential aliasing.)

4) For the method transfer in BankAccount.java, try to establish
   that the balance of neither bank account will change if
   this method throws a DebitException.

5) In the class Person.java, use an owner field to specify 
   that the account is "owned" by a Person.

   Ie declare an invariant
     //@ invariant account.owner == this;
   in class Person, and add
     //@ set account.owner = this;
   after the creation of the account to set its owner field.

   If you've done this correctly, a precondition 
    //@ requires p != this;
   for the method transfer in Person should suffice to prove the 
   assertion 
    //@ assert account != p.account;
   in this method.