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