indexing description: "Simple bank account" author: "Peter Brandt and Martin Geisler" date: "$Date: 2005-06-25 13:49:03 +0200 (Sat, 25 Jun 2005) $" revision: "$Revision: 97 $" class ACCOUNT create make feature {NONE} -- Initialization make (initial_balance: DOUBLE) is -- Creation procedure require initial_balance_non_negative: initial_balance >= 0 do debug ("save_states") (create {STATE_MANAGER}).save_state (Current, "make", [initial_balance]) end balance := initial_balance ensure initial_balance_set: balance = initial_balance end feature -- Status report balance: DOUBLE -- Balance of the account feature -- Basic operations deposit (sum: DOUBLE) is -- Add `sum' to `balance' require sum_non_negative: sum >= 0 do debug ("save_states") (create {STATE_MANAGER}).save_state (Current, "deposit", [sum]) end balance := balance + sum ensure balance_updated: balance = old balance + sum end withdraw (sum: DOUBLE) is -- Subtract `sum' from `balance' require sum_non_negative: sum >= 0 not_too_big: sum <= balance do debug ("save_states") (create {STATE_MANAGER}).save_state (Current, "withdraw", [sum]) end balance := balance - sum ensure balance_updated: balance = old balance - sum end invariant balance_non_negative: balance >= 0 end -- class ACCOUNT