note description: "Summary description for {PERSON}." author: "" date: "$Date$" revision: "$Revision$" class PERSON create make feature -- Access surname: STRING_8 assign set_surname -- Nachname firstname: STRING_8 assign set_firstname -- Vorname feature {NONE} -- Initialization make (a_surname: like surname; a_firstname: like firstname) do surname := a_surname firstname := a_firstname end feature {NONE} -- Implementation set_surname (a_surname: like surname) -- Assign `surname' with `a_surname'. require a_surname_not_empty: 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: not a_firstname.is_empty do firstname := a_firstname ensure firstname_assigned: firstname = a_firstname end invariant firstname_not_empty: not firstname.is_empty surname_not_empty: not surname.is_empty end