bank-eiffel/person.e


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54

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