deferred class interface DS_INDEXABLE[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_SORTABLE -- Status report sorted (a_sorter: DS_SORTER[G]): BOOLEAN -- Is container sorted according to a_sorter's criterion? require a_sorter_not_void: a_sorter /= Void feature(s) from DS_SORTABLE -- Sort sort (a_sorter: DS_SORTER[G]) -- Sort container using a_sorter's algorithm. require a_sorter_not_void: a_sorter /= Void ensure sorted: sorted(a_sorter) feature(s) from DS_INDEXABLE -- Access infix "@" (i: INTEGER): G -- Item at index i require valid_index: 1 <= i and i <= count feature(s) from DS_INDEXABLE -- Access item (i: INTEGER): G -- Item at index i require valid_index: 1 <= i and i <= count first: G -- First item in container require not_empty: not is_empty ensure definition: Result = item(1) last: G -- Last item in container require not_empty: not is_empty ensure definition: Result = item(count) feature(s) from DS_INDEXABLE -- Status report extendible (n: INTEGER): BOOLEAN -- May container be extended with n items? require positive_n: n >= 0 feature(s) from DS_INDEXABLE -- Element change put_first (v: G) -- Add v to beginning of container. require extendible: extendible(1) ensure one_more: count = old count + 1; inserted: first = v put_last (v: G) -- Add v to end of container. require extendible: extendible(1) ensure one_more: count = old count + 1; inserted: last = v put (v: G; i: INTEGER) -- Add v at i-th position. require extendible: extendible(1); valid_index: 1 <= i and i <= count + 1 ensure one_more: count = old count + 1; inserted: item(i) = v force_first (v: G) -- Add v to beginning of container. ensure one_more: count = old count + 1; inserted: first = v force_last (v: G) -- Add v to end of container. ensure one_more: count = old count + 1; inserted: last = v force (v: G; i: INTEGER) -- Add v at i-th position. require valid_index: 1 <= i and i <= count + 1 ensure one_more: count = old count + 1; inserted: item(i) = v replace (v: G; i: INTEGER) -- Replace item at i-th position by v. require valid_index: 1 <= i and i <= count ensure same_count: count = old count; replaced: item(i) = v swap (i, j: INTEGER) -- Exchange items at indexes i and j. require valid_i: 1 <= i and i <= count; valid_j: 1 <= j and j <= count ensure same_count: count = old count; new_i: item(i) = old item(j); new_j: item(j) = old item(i) extend_first (other: DS_LINEAR[G]) -- Add items of other to beginning of container. -- Keep items of other in the same order. require other_not_void: other /= Void; extendible: extendible(other.count) ensure new_count: count = old count + other.count; same_order: not other.is_empty implies first = other.first extend_last (other: DS_LINEAR[G]) -- Add items of other to end of container. -- Keep items of other in the same order. require other_not_void: other /= Void; extendible: extendible(other.count) ensure new_count: count = old count + other.count; same_order: not other.is_empty implies item(old count + 1) = other.first extend (other: DS_LINEAR[G]; i: INTEGER) -- Add items of other at i-th position. -- Keep items of other in the same order. require other_not_void: other /= Void; extendible: extendible(other.count); valid_index: 1 <= i and i <= count + 1 ensure new_count: count = old count + other.count; same_order: not other.is_empty implies item(i) = other.first append_first (other: DS_LINEAR[G]) -- Add items of other to beginning of container. -- Keep items of other in the same order. require other_not_void: other /= Void ensure new_count: count = old count + other.count; same_order: not other.is_empty implies first = other.first append_last (other: DS_LINEAR[G]) -- Add items of other to end of container. -- Keep items of other in the same order. require other_not_void: other /= Void ensure new_count: count = old count + other.count; same_order: not other.is_empty implies item(old count + 1) = other.first append (other: DS_LINEAR[G]; i: INTEGER) -- Add items of other at i-th position. -- Keep items of other in the same order. require other_not_void: other /= Void; valid_index: 1 <= i and i <= count + 1 ensure new_count: count = old count + other.count; same_order: not other.is_empty implies item(i) = other.first feature(s) from DS_INDEXABLE -- Removal remove_first -- Remove first item from container. require not_empty: not is_empty ensure one_less: count = old count - 1 remove_last -- Remove last item from container. require not_empty: not is_empty ensure one_less: count = old count - 1 remove (i: INTEGER) -- Remove item at i-th position. require not_empty: not is_empty; valid_index: 1 <= i and i <= count ensure one_less: count = old count - 1 prune_first (n: INTEGER) -- Remove n first items from container. require valid_n: 0 <= n and n <= count ensure new_count: count = old count - n prune_last (n: INTEGER) -- Remove n last items from container. require valid_n: 0 <= n and n <= count ensure new_count: count = old count - n prune (n: INTEGER; i: INTEGER) -- Remove n items at and after i-th position. require valid_index: 1 <= i and i <= count; valid_n: 0 <= n and n <= count - i + 1 ensure new_count: count = old count - n keep_first (n: INTEGER) -- Keep n first items in container. require valid_n: 0 <= n and n <= count ensure new_count: count = n keep_last (n: INTEGER) -- Keep n last items in container. require valid_n: 0 <= n and n <= count ensure new_count: count = n invariant positive_count: count >= 0; empty_definition: is_empty = count = 0; end of deferred DS_INDEXABLE[G]