/*@ requires amt > 0 && amt <= bal;
    @ assignable bal;
    @ ensures bal == \old(bal) - amt; @*/
  public void withdraw(int amt) {
    if (amt > bal && amt <= bal){
    	bal -= amt;
    } else {
    	//raise what ?
    }

  }