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.