blob: 5230362e9f994c352b6ee45516fc3302c418b0ba (
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
|
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
|
