note description: "Summary description for {ACCOUNT}." author: "" date: "$Date$" revision: "$Revision$" class interface ACCOUNT create make feature -- basic operations balance: MONEY deposit (m: MONEY) require m >= m.zero ensure balance = old balance + m withdraw (m: MONEY) require m.zero <= m and m <= balance ensure balance = old balance - m feature -- transfer transfer (percent: INTEGER_32; a: ACCOUNT) -- percent is an integer between 0 and 100 -- transfer percent of current to account a without losing pennies require percent_between_zero_and_100: 0 <= percent and percent <= 100 ensure transfer_conserves_money: balance + a.balance = old (balance + a.balance) correct_other_balance: a.balance = old (a.balance + allocate_by (percent)) correct_current_balance: balance = old (balance - allocate_by (percent)) allocate_by (percent: INTEGER_32): MONEY ensure Result = balance.allocated_by_ratios (create {NUM_ARRAY [INTEGER_32]}.from_array (<<percent, 100 - percent>>)) [1] invariant balance >= balance.zero end -- class ACCOUNT
Generated by ISE EiffelStudio