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