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