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