Variations on the Toy Electronic Purse

Here are some additional code to the Purse example:

0pt //@+ CheckArithOverflow = no

class NoCreditException extends Exception {

public NoCreditException() { }

public class Purse {

private int balance;

//@ invariant balance_positive: balance > 0;

/*@ requires amount > 0;
@
assigns balance;
@
ensures balance == amount;
@*/

public Purse(int amount) {
balance = amount;
}

/*@ requires s >= 0;
@
assigns balance;
@
ensures balance == \old(balance) + s;
@*/

public void credit(int s) {
balance += s;
}

/*@ requires s >= 0;
@
assigns balance;
@
ensures s < \old(balance) && balance == \old(balance)  s;
@
behavior amount_too_large:
@
assigns \nothing
@
signals (NoCreditException) s >= \old(balance) ;
@*/

public void withdraw(int s) throws NoCreditException {

if (s < balance)
balance = balance
- s;

else
throw
new NoCreditException();
}

/*@ assigns p1.balance,p2.balance;
@
ensures \result == 50;
@*/

public static int test1(Purse p1, Purse p2) {
p1.balance = 50;
p2.credit(100);

return p1.balance;
}

/*@ assigns \nothing
@
ensures \result == 150;
@
behavior impossible:
@
signals (NoCreditException) false;
@*/

public static int test2() throws NoCreditException {
Purse p1 =
new Purse(100);
Purse p2 =
new Purse(200);
p1.withdraw(50);
p2.withdraw(100);

return p1.balance+p2.balance;
}

/*@ requires p != null;
@
behavior transfer_ok:
@   assumes p != this;
@
assigns this.balance, p.balance;
@
ensures \result == \old(balance) + s;
@
behavior transfer_cancelled:
@
assigns \nothing
@
signals (NoCreditException) true;
@*/

public int transfer(Purse p, int s) throws NoCreditException {
balance += s;
p.withdraw(s);

return balance;
}

1. Fix the annotations of methods `test1` and `test2`
2. Fix the bug in the code of `transfer`

This document was translated from LATEX by HEVEA.