object account is
  functions
   bal : account -> money
  methods
   credit : account * money -> account
   debit : account * money -> account
  error
   overdraw : money -> money
  axioms
   bal(new(A)) = 0
   bal(credit(A,M)) = bal(A) + M
   bal(debit(A,M)) = bal(A) - M if bal(A) >= M
  error-axioms
   bal(debit(A,M)) = overdraw(M) if bal(A) < M
  end