note
description: "Simple bank accounts"

class
ACCOUNT

feature

balance: INTEGER -- Current balance

deposit (sum: INTEGER)
  -- Add `sum' to account.
  require
  non_negative: sum >= 0
  do
  balance := balance + sum
  ensure
  --one_more_deposit: deposit_count = old deposit_count + 1
  updated: balance = old balance + sum
  end