context PayCard::charge(amount: Integer)
  pre :   balance + amount < limit and amount >=0
  post :  balance = balance@pre + amount