diff options
Diffstat (limited to 'bank-eiffel/person.e')
| -rw-r--r-- | bank-eiffel/person.e | 16 |
1 files changed, 4 insertions, 12 deletions
diff --git a/bank-eiffel/person.e b/bank-eiffel/person.e index 54e1a45..ffaab72 100644 --- a/bank-eiffel/person.e +++ b/bank-eiffel/person.e | |||
| @@ -1,9 +1,3 @@ | |||
| 1 | note | ||
| 2 | description: "Summary description for {PERSON}." | ||
| 3 | author: "" | ||
| 4 | date: "$Date$" | ||
| 5 | revision: "$Revision$" | ||
| 6 | |||
| 7 | class | 1 | class |
| 8 | PERSON | 2 | PERSON |
| 9 | 3 | ||
| @@ -14,11 +8,9 @@ feature -- Access | |||
| 14 | 8 | ||
| 15 | surname: STRING_8 assign set_surname | 9 | surname: STRING_8 assign set_surname |
| 16 | -- Nachname | 10 | -- Nachname |
| 17 | attribute Result := ({like surname}).default end --| Remove line when Void Safety is properly set | ||
| 18 | 11 | ||
| 19 | firstname: STRING_8 assign set_firstname | 12 | firstname: STRING_8 assign set_firstname |
| 20 | -- Vorname | 13 | -- Vorname |
| 21 | attribute Result := ({like firstname}).default end --| Remove line when Void Safety is properly set | ||
| 22 | 14 | ||
| 23 | feature {NONE} -- Initialization | 15 | feature {NONE} -- Initialization |
| 24 | 16 | ||
| @@ -33,7 +25,7 @@ feature {NONE} -- Implementation | |||
| 33 | set_surname (a_surname: like surname) | 25 | set_surname (a_surname: like surname) |
| 34 | -- Assign `surname' with `a_surname'. | 26 | -- Assign `surname' with `a_surname'. |
| 35 | require | 27 | require |
| 36 | a_surname_not_empty: a_surname /= Void and then not a_surname.is_empty | 28 | a_surname_not_empty: not a_surname.is_empty |
| 37 | do | 29 | do |
| 38 | surname := a_surname | 30 | surname := a_surname |
| 39 | ensure | 31 | ensure |
| @@ -43,7 +35,7 @@ feature {NONE} -- Implementation | |||
| 43 | set_firstname (a_firstname: like firstname) | 35 | set_firstname (a_firstname: like firstname) |
| 44 | -- Assign `firstname' with `a_firstname'. | 36 | -- Assign `firstname' with `a_firstname'. |
| 45 | require | 37 | require |
| 46 | a_firstname_not_empty: a_firstname /= Void and then not a_firstname.is_empty | 38 | a_firstname_not_empty: not a_firstname.is_empty |
| 47 | do | 39 | do |
| 48 | firstname := a_firstname | 40 | firstname := a_firstname |
| 49 | ensure | 41 | ensure |
| @@ -51,6 +43,6 @@ feature {NONE} -- Implementation | |||
| 51 | end | 43 | end |
| 52 | 44 | ||
| 53 | invariant | 45 | invariant |
| 54 | firstname_not_empty: firstname /= Void and then not firstname.is_empty | 46 | firstname_not_empty: not firstname.is_empty |
| 55 | surname_not_empty: surname /= Void and then not surname.is_empty | 47 | surname_not_empty: not surname.is_empty |
| 56 | end | 48 | end |
