indexing
	description: "Simple employee with a name, an age, and an associated `ACCOUNT' object"
	author: "Peter Brandt and Martin Geisler"
	date: "$Date: 2005-06-25 13:49:03 +0200 (Sat, 25 Jun 2005) $"
	revision: "$Revision: 97 $"

class
	EMPLOYEE

create
	make

feature {NONE} -- Initialization

	make (an_account: ACCOUNT; a_name: STRING; an_age: INTEGER) is
			-- Creation procedure.
		require
			an_account_not_void: an_account /= Void
			a_name_not_void: a_name /= Void
			an_age_positive: an_age > 0
		do
				debug ("save_states")
					(create {STATE_MANAGER}).save_state (Current, "make", [an_account, a_name, an_age])
				end
			salary_account := an_account
			name := a_name
			age := an_age
		ensure
			salary_account_set: salary_account = an_account
			name_set: name = a_name
			age_set: age = an_age
		end

feature -- Status report

	pension_rate: DOUBLE is 0.1
		-- Pension rate
	
	health_insurance: DOUBLE is 200.0
		-- Halth insurance premium

feature -- Basic operations

	receive_salary (sum: INTEGER) is
			-- Deposit `sum' in salary account, deducing taxes
		require
			sum_positive: sum > 0
		do
				debug ("save_states")
					(create {STATE_MANAGER}).save_state (Current, "receive_salary", [sum])
				end
			salary_account.deposit(sum - tax (sum))
		end

	tax (sum: INTEGER): DOUBLE is
			-- Taxes that must be paid for `sum'
		require
			sum_positive: sum > 0
		do
				debug ("save_states")
					(create {STATE_MANAGER}).save_state (Current, "tax", [sum])
				end
			Result := health_insurance + pension_rate*sum
		ensure
			tax_non_negative: Result >= 0
			tax_less_than_sum: Result <= sum
		end

feature {NONE} -- Implementation
	name: STRING
		-- Employee name
	age: INTEGER
		-- Employee age
	salary_account: ACCOUNT
		-- Employee salery account

invariant
	salary_account_not_void: salary_account /= Void
	name_not_void: name /= Void
	age_positive: age > 0

end -- class EMPLOYEE