class
	BASE

feature
	add10(num: INTEGER): INTEGER
		require
			base_always_false: false -- always false
		do
			RESULT := num + 10
		ensure
			base_always_true: true
		end
end