deferred class TEST1
feature
	make
		do
			create center
		end

	is_center_valid: BOOLEAN

	x: INTEGER
		do
			if not is_center_valid then
				set_center
			end
			Result := center.x
		end

	set_center
		deferred
		ensure
			center_valid: is_center_valid
		end

	center: CENTER
	
invariant
	center_exists: center /= Void
	set: x = center.x

end