blob: ffaab7289e1e26bd7d40f469427ef6082e68b0a3 (
plain)
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
|
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
|
