eiffel-fragen/replaceability/derived.e


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

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
			-- my postcondition
			derived_result_equals_myresult: RESULT = myresult
		end

	myresult: INTEGER
		do
			RESULT := 110
		end
end