Is Empty Code template contract predicate to ensure a finite entity is empty Eiffel Software is_empty Eiffel code contract precondition postcondition An attached variable with access to an `is_empty' status function