eiffel-fragen/nachbedingung/child.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
               CHILD
inherit
	COUNTER
		redefine
			set,
			checkval
	    end

feature -- Element change

    set (some_value: INTEGER) is
            -- Set value of counter to some_value.
             do
                         item := some_value - 10
             ensure then
             			 checkval > 0
             end

    checkval: INTEGER is
    		-- Get value of counter
    		do
    			Result := item + 20
    		end
end