blob: 0622d41e34104af0e0341333e691400a280ddba1 (
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
|
class
DERIVED2
inherit
BASE
redefine add10 select add10
end
DERIVED
rename add10 as derived_add10
redefine myresult
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
myresult: INTEGER
do
RESULT := 20
end
end
|
