class
	TEST

create
	run

feature {NONE} -- Initialization

	run
		local
			base: BASE
			derived: DERIVED
			derived2: DERIVED2
			ret: INTEGER
		do
			create base
			create derived
			create derived2

			ret := derived.add10(100) -- works
			--ret := derived2.add10(100) -- fails due to stronger preconditions

			--ret := derived.add10(10) -- fails due to postcondition
			ret := derived2.add10(10) -- works due to weaker postcondition
		end
end