note
	description: "Summary description for {ACCOUNT}."
	author: ""
	date: "$Date$"
	revision: "$Revision$"

class 
	ACCOUNT

create 
	make

feature {NONE} -- create

	make
			-- a new account
		do
			create balance.make_from_int (0)
		ensure
				balance = balance.zero
		end
	
feature -- basic operations

	balance: MONEY

	deposit (m: MONEY)
		require
				m >= m.zero
		do
			balance := balance + m
		ensure
				balance = old balance + m
		end

	withdraw (m: MONEY)
		require
				m.zero <= m and m <= balance
		do
			balance := balance - m
		ensure
				balance = old balance - m
		end
	
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
		local
			na: MONEY_ARRAY
			ratio1, ratio2: INTEGER_32
		do
			ratio1 := percent
			ratio2 := 100 - percent
			na := balance.allocated_by_ratios (create {NUM_ARRAY [INTEGER_32]}.from_array (<<ratio1, ratio2>>))
			a.deposit (na [1])
			balance := balance - na [1]
		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))
		end

	allocate_by (percent: INTEGER_32): MONEY
		do
			Result := balance.allocated_by_ratios (create {NUM_ARRAY [INTEGER_32]}.from_array (<<percent, 100 - percent>>)) [1]
		ensure
				Result = balance.allocated_by_ratios (create {NUM_ARRAY [INTEGER_32]}.from_array (<<percent, 100 - percent>>)) [1]
		end
	
invariant
		balance >= balance.zero

end -- class ACCOUNT

Generated by ISE EiffelStudio