//Example from page 339
//comments on the problem section
//line 1   : definition of   balance@pre
//line 2   : precondition
//line 3-4 : invariant. \phi in Template 5
//line 5   : {self.balance:=l_balance(self)} is
//            the anonymizing update 
//line 6   : postcondition
//line 7   : anonymizing update 
//line 8-9 : invariant
//

\javaSource "paycardChapt8";

\functions {
  int balance@pre(PayCard);
  int l_balance(PayCard);
  PayCard self;
  boolean created(PayCard);
}

\programVariables {
  int amount;
}
\problem {
  (\forall PayCard pc; balance@pre(pc)= pc.balance)
& self.balance + amount < self.limit & amount >= 0 
& (\forall PayCard pc; (pc.<created>=TRUE -> 0 <= pc.balance 
                       & pc.balance <= pc.limit))
& {self.balance:=l_balance(self)} 
            self.balance = balance@pre(self) + amount
-> {self.balance:=l_balance(self)} 
   (\forall PayCard pc; (pc.<created>=TRUE -> 0 <= pc.balance 
                       & pc.balance <= pc.limit))
}