blob: 7f23f15c63b58e60482ea1519a93bca71eb69aec (
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
|
class
DERIVED2
inherit
BASE
redefine add10 select add10
end
DERIVED
rename add10 as derived_add10
redefine mypostcondition
end
feature
add10(num: INTEGER): INTEGER
require else
-- stronger precondition
derived2_num_between_1_and_10: num >= 1 and num <= 10
do
RESULT := derived_add10(num)
end
-- weaken postcondition
mypostcondition(num: INTEGER): BOOLEAN
do
Result := false
if Precursor(num) or num = 20 then
Result := true
end
end
end
|
