/* ESC/Java may complain about this class, but ignore this */

public class DebitException extends RuntimeException {

  //@ assignable \nothing;
  public /*@ pure @*/ DebitException(){ 
    super("Action not executed because insuffient funds");
  } 

}