All Items Deattached Code template contract predicate to ensure a chained container structure has only detached items Eiffel Software all_detached Eiffel code contract invariant precondition postcondition An attached chain container entity