note description: "Summary description for {PERSON}." author: "" date: "$Date$" revision: "$Revision$" class PERSON create make feature {NONE} -- Initialization surname: STRING_8 -- Nachname attribute Result := ({like surname}).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 make (a_surname: like surname; a_firstname: like firstname) do set_surname (a_surname) set_firstname (a_firstname) end set_surname (a_surname: like surname) -- Assign `surname' with `a_surname'. require a_surname_not_empty: a_surname /= Void and then not a_surname.is_empty do surname := a_surname ensure surname_assigned: surname = a_surname 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 surname_not_empty: surname /= Void and then not surname.is_empty end