package demo_purse;

class Purse {
    
    public int balance;
    //@ public invariant balance >= 0; 

    /*@ public normal_behavior
      @   requires s >= 0;
      @   assigns balance;
      @   ensures balance == \old(balance)+s;
      @*/
    public void credit(int s) {
	balance += s;
    }

    /*@ public behavior
      @   requires s >= 0;
      @   assigns balance;
      @   ensures s <= \old(balance) && 
      @     balance == \old(balance) - s;
      @   signals (NoCreditException) 
      @      s > \old(balance) && 
      @      balance == \old(balance); 
      @*/
    public void withdraw(int s) throws NoCreditException {
	if (balance >= s) balance -= s;
	else throw new NoCreditException();
    }

    /*@ public normal_behavior
      @   requires p1.balance==100 && p1 != null && p2 != null 
          && p1 != p2 && p2.balance >= 100;
      @   ensures \result == 150;
      @*/
    public static int test(Purse p1, Purse p2) {
	p1.credit(50);
	p2.withdraw(100);
	return p1.balance;
    }

}


class NoCreditException extends Exception {

    /*@ public normal_behavior
      @   assigns \nothing;
      @*/
    public NoCreditException() {}
}