blob: b13300f89b21d8af03138e8cb4a15a8f70d9765c (
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
|
class
DERIVED
inherit
BASE
redefine add10
end
feature
add10(num: INTEGER): INTEGER
require else
-- my precondition
derived_num_positive: num > 0
do
RESULT := num + 10
ensure then
derived_result_equals_mypostcondition: mypostcondition(RESULT)
end
-- my postcondition
mypostcondition(num: INTEGER): BOOLEAN
do
Result := false
if num = 110 then
Result := true
end
end
end
|
