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