| Class DS_INDEXABLE |
note
description:
"Data structures that can be traversed and %
%modified through integer access"
library: "Gobo Eiffel Structure Library"
author: "Eric Bezault <ericb@gobosoft.com>"
copyright: "Copyright (c) 1999-2001, Eric Bezault and others"
license: "MIT License"
deferred class interface
DS_INDEXABLE [G]
inherit
DS_SORTABLE [G]
DS_CONTAINER [G]
feature {NONE} -- Initialization
make_default
-- Create an empty container.
-- (From DS_CONTAINER.)
deferred
ensure
empty: is_empty
feature -- Access
infix "@", item (i: INTEGER): G -- Item at index i require valid_index: 1 <= i and i <= count deferredfirst: G -- First item in container require not_empty: not is_empty deferred ensure definition: Result = item (1)last: G -- Last item in container require not_empty: not is_empty deferred ensure definition: Result = item (count)
feature -- Measurement
count: INTEGER
-- Number of items in container
-- (From DS_CONTAINER.)
deferred
feature -- Status report
is_empty: BOOLEAN -- Is container empty? -- (From DS_CONTAINER.)extendible (n: INTEGER): BOOLEAN -- May container be extended with n items? require positive_n: n >= 0 deferredsorted (a_sorter: DS_SORTER [G]): BOOLEAN -- Is container sorted according to a_sorter's criterion? -- (From DS_SORTABLE.) require a_sorter_not_void: a_sorter /= Void
feature -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is current container equal to other?
-- (From GENERAL.)
require
other_not_void: other /= Void
deferred
ensure
consistent: standard_is_equal (other) implies Result
same_type: Result implies same_type (other)
symmetric: Result implies other.is_equal (Current)
same_count: Result implies count = other.count
feature -- Duplication
copy (other: like Current)
-- Copy other to current container.
-- (From GENERAL.)
require
other_not_void: other /= Void
type_identity: same_type (other)
deferred
ensure
is_equal: is_equal (other)
feature -- Sort
sort (a_sorter: DS_SORTER [G])
-- Sort container using a_sorter's algorithm.
-- (From DS_SORTABLE.)
require
a_sorter_not_void: a_sorter /= Void
ensure
sorted: sorted (a_sorter)
feature -- Element change
put_first (v: G) -- Add v to beginning of container. require extendible: extendible (1) deferred ensure one_more: count = old count + 1 inserted: first = vput_last (v: G) -- Add v to end of container. require extendible: extendible (1) deferred ensure one_more: count = old count + 1 inserted: last = vput (v: G; i: INTEGER) -- Add v at i-th position. require extendible: extendible (1) valid_index: 1 <= i and i <= (count + 1) deferred ensure one_more: count = old count + 1 inserted: item (i) = vforce_first (v: G) -- Add v to beginning of container. deferred ensure one_more: count = old count + 1 inserted: first = vforce_last (v: G) -- Add v to end of container. deferred ensure one_more: count = old count + 1 inserted: last = vforce (v: G; i: INTEGER) -- Add v at i-th position. require valid_index: 1 <= i and i <= (count + 1) deferred ensure one_more: count = old count + 1 inserted: item (i) = vreplace (v: G; i: INTEGER) -- Replace item at i-th position by v. require valid_index: 1 <= i and i <= count deferred ensure same_count: count = old count replaced: item (i) = vswap (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) deferred 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) deferred 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) deferred 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 deferred 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 deferred 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) deferred ensure new_count: count = old count + other.count same_order: (not other.is_empty) implies (item (i) = other.first)
feature -- Removal
remove_first -- Remove first item from container. require not_empty: not is_empty deferred ensure one_less: count = old count - 1remove_last -- Remove last item from container. require not_empty: not is_empty deferred ensure one_less: count = old count - 1remove (i: INTEGER) -- Remove item at i-th position. require not_empty: not is_empty valid_index: 1 <= i and i <= count deferred ensure one_less: count = old count - 1prune_first (n: INTEGER) -- Remove n first items from container. require valid_n: 0 <= n and n <= count deferred ensure new_count: count = old count - nprune_last (n: INTEGER) -- Remove n last items from container. require valid_n: 0 <= n and n <= count deferred ensure new_count: count = old count - nprune (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) deferred ensure new_count: count = old count - nkeep_first (n: INTEGER) -- Keep n first items in container. require valid_n: 0 <= n and n <= count deferred ensure new_count: count = nkeep_last (n: INTEGER) -- Keep n last items in container. require valid_n: 0 <= n and n <= count deferred ensure new_count: count = nwipe_out -- Remove all items from container. -- (From DS_CONTAINER.) deferred ensure wiped_out: is_empty
invariant
positive_count: count >= 0
empty_definition: is_empty = (count = 0)
-- (From DS_CONTAINER.)
end -- class DS_INDEXABLE
|
Copyright © 1999-2001, Eric
Bezault mailto:ericb@gobosoft.com http://www.gobosoft.com Last Updated: 31 March 2001 |