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