diff options
Diffstat (limited to 'eiffel-fragen')
| -rw-r--r-- | eiffel-fragen/replaceability/derived.e | 11 | ||||
| -rw-r--r-- | eiffel-fragen/replaceability/derived2.e | 9 |
2 files changed, 13 insertions, 7 deletions
diff --git a/eiffel-fragen/replaceability/derived.e b/eiffel-fragen/replaceability/derived.e index 9a409bd..b13300f 100644 --- a/eiffel-fragen/replaceability/derived.e +++ b/eiffel-fragen/replaceability/derived.e | |||
| @@ -14,12 +14,15 @@ feature | |||
| 14 | do | 14 | do |
| 15 | RESULT := num + 10 | 15 | RESULT := num + 10 |
| 16 | ensure then | 16 | ensure then |
| 17 | -- my postcondition | 17 | derived_result_equals_mypostcondition: mypostcondition(RESULT) |
| 18 | derived_result_equals_myresult: RESULT = myresult | ||
| 19 | end | 18 | end |
| 20 | 19 | ||
| 21 | myresult: INTEGER | 20 | -- my postcondition |
| 21 | mypostcondition(num: INTEGER): BOOLEAN | ||
| 22 | do | 22 | do |
| 23 | RESULT := 110 | 23 | Result := false |
| 24 | if num = 110 then | ||
| 25 | Result := true | ||
| 26 | end | ||
| 24 | end | 27 | end |
| 25 | end | 28 | end |
diff --git a/eiffel-fragen/replaceability/derived2.e b/eiffel-fragen/replaceability/derived2.e index 0622d41..7f23f15 100644 --- a/eiffel-fragen/replaceability/derived2.e +++ b/eiffel-fragen/replaceability/derived2.e | |||
| @@ -7,7 +7,7 @@ inherit | |||
| 7 | end | 7 | end |
| 8 | DERIVED | 8 | DERIVED |
| 9 | rename add10 as derived_add10 | 9 | rename add10 as derived_add10 |
| 10 | redefine myresult | 10 | redefine mypostcondition |
| 11 | end | 11 | end |
| 12 | 12 | ||
| 13 | feature | 13 | feature |
| @@ -20,8 +20,11 @@ feature | |||
| 20 | end | 20 | end |
| 21 | 21 | ||
| 22 | -- weaken postcondition | 22 | -- weaken postcondition |
| 23 | myresult: INTEGER | 23 | mypostcondition(num: INTEGER): BOOLEAN |
| 24 | do | 24 | do |
| 25 | RESULT := 20 | 25 | Result := false |
| 26 | if Precursor(num) or num = 20 then | ||
| 27 | Result := true | ||
| 28 | end | ||
| 26 | end | 29 | end |
| 27 | end | 30 | end |
