deferred class interface DS_RESIZABLE[G] feature(s) from DS_CONTAINER -- Measurement count: INTEGER -- Number of items in container feature(s) from DS_CONTAINER -- Status report is_empty: BOOLEAN -- Is container empty? feature(s) from DS_CONTAINER -- Comparison is_equal (other: like Current): BOOLEAN -- Is current container equal to other? require other_not_void: other /= Void ensure consistent: standard_is_equal(other) implies Result; symmetric: Result implies other.is_equal(Current) feature(s) from DS_CONTAINER -- Removal wipe_out -- Remove all items from container. ensure wiped_out: is_empty feature(s) from DS_RESIZABLE -- Measurement capacity: INTEGER -- Maximum number of items in container feature(s) from DS_RESIZABLE -- Status report is_full: BOOLEAN -- Is container full? feature(s) from DS_RESIZABLE -- Resizing resize (n: INTEGER) -- Resize container so that it can contain -- at least n items. Do not lose any item. require n_large_enough: n >= capacity ensure capacity_set: capacity = n invariant positive_count: count >= 0; empty_definition: is_empty = count = 0; count_constraint: count <= capacity; full_definition: is_full = count = capacity; end of deferred DS_RESIZABLE[G]