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

class
	PERSON

feature -- Access

	surename: STRING_8
			-- Nachname
		attribute Result := ({like surename}).default end --| Remove line when Void Safety is properly set

	firstname: STRING_8 assign set_firstname
			-- Vorname
		attribute Result := ({like firstname}).default end --| Remove line when Void Safety is properly set

feature -- Element change

	set_surename (a_surename: like surename)
			-- Assign `surename' with `a_surename'.
		require
			a_surename_not_empty: a_surename /= Void and then not a_surename.is_empty
		do
			surename := a_surename
		ensure
			surename_assigned: surename = a_surename
		end

	set_firstname (a_firstname: like firstname)
			-- Assign `firstname' with `a_firstname'.
		require
			a_firstname_not_empty: a_firstname /= Void and then not a_firstname.is_empty
		do
			firstname := a_firstname
		ensure
			firstname_assigned: firstname = a_firstname
		end

invariant
	firstname_not_empty: firstname /= Void and then not firstname.is_empty
	surename_not_empty: surename /= Void and then not surename.is_empty
end