Is Detached or Empty Code template contract predicate to ensure a finite entity is detached or is empty Eiffel Software is_detached_or_empty Eiffel code contract precondition postcondition A variable with access to an `is_empty' status function