indexing
description: "Simple single-linked lists"
author: "Patrick Schoenbach"
access: cursor
representation: linked
contents: generic
class interface
SIMPLE_LIST [G]
create
make
require
empty: empty
feature -- Access
index: INTEGER
-- Current index
-- (from LIST_ADAPTER)
i_th (i: INTEGER): G
-- Item at index i
-- Was declared in DS_LINKED_LIST as synonym of @ and item.
-- (from DS_LINKED_LIST)
require -- from SEQUENCIAL_CONTAINER
valid_index: valid_index (i)
require -- from DS_TABLE
valid_entry: valid_entry (k)
item: G
-- Current item
-- (from LIST_ADAPTER)
require -- from SEQUENCIAL_CONTAINER
not_off: not off
feature -- Measurement
capacity: INTEGER
-- Capacity of list
-- (from LIST_ADAPTER)
count: INTEGER
-- Number of items in list
-- (from DS_LINKED_LIST)
feature -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is list equal to other?
-- (from DS_LINKED_LIST)
require -- DS_CONTAINER
precursor: True
require -- from GENERAL
other_not_void: other /= void
ensure then -- from DS_CONTAINER
same_count: Result implies count = other.count
ensure -- from GENERAL
symmetric: Result implies other.is_equal (Current);
consistent: standard_is_equal (other) implies Result
feature -- Status report
after: BOOLEAN
-- Is there no valid item to the left of cursor?
-- (from LIST_ADAPTER)
before: BOOLEAN
-- Is there no valid item to the right of cursor?
-- (from LIST_ADAPTER)
Full: BOOLEAN is false
-- Is container full? (Answer: no)
-- (from LIST_ADAPTER)
Insertable: BOOLEAN is true
-- Can items be inserted in the middle of container? (Answer: yes)
-- (from LIST_ADAPTER)
empty: BOOLEAN
-- Is structure empty?
-- (from DS_CONTAINER)
isfirst: BOOLEAN
-- Is cursor on first item?
-- (from LIST_ADAPTER)
islast: BOOLEAN
-- Is cursor on last item?
-- (from LIST_ADAPTER)
off: BOOLEAN
-- Is cursor off the list?
-- (from LIST_ADAPTER)
Prunable: BOOLEAN is true
-- Can items be removed from container? (Answer: yes)
-- (from LIST_ADAPTER)
Resizable: BOOLEAN is false
-- Can container be resized? (Answer: no)
-- (from LIST_ADAPTER)
valid_index (i: INTEGER): BOOLEAN
-- Is i a valid index?
-- (from DS_INDEXABLE)
ensure then -- from DS_INDEXABLE
definition: Result = (1 <= i and i <= count + 1)
ensure then -- from DS_INDEXABLE
definition: Result = (1 <= i and i <= count + 1)
feature -- Cursor movement
forth
-- Move cursor forwards.
-- (from LIST_ADAPTER)
require -- from SEQUENCIAL_CONTAINER
not_after: not after
ensure then -- from LINEAR_CONTAINER
next_position: index = old index + 1
go_i_th (i: INTEGER)
-- Move cursor to i-th item.
-- (from LIST_ADAPTER)
require -- from SEQUENCIAL_CONTAINER
valid_index: valid_index (i)
ensure -- from SEQUENCIAL_CONTAINER
i_th_position: index = i
start
-- Move cursor to first item.
-- (from LIST_ADAPTER)
require -- from SEQUENCIAL_CONTAINER
not_empty: not empty
ensure -- from SEQUENCIAL_CONTAINER
cursor_at_start: isfirst
feature -- Element change
extend (v: G)
-- Add v to end of container.
-- (from LIST_ADAPTER)
require -- from SEQUENCIAL_CONTAINER
not_full: not full
ensure then -- from LINEAR_CONTAINER
extended: i_th (count) = v;
count_increased: count = old count + 1;
index_unchanged: not old empty implies index = old index
put (v: G)
-- Replace current item with v.
-- (from LIST_ADAPTER)
require -- from SEQUENCIAL_CONTAINER
not_off: not off
ensure then -- from LINEAR_CONTAINER
replaced: item = v;
count_unchanged: count = old count;
index_unchanged: index = old index
put_left (v: G)
-- Insert v to the left of current position.
-- (from LIST_ADAPTER)
require -- from SEQUENCIAL_CONTAINER
insertable: insertable;
not_full: not full;
not_before: not before
ensure then -- from LINEAR_CONTAINER
inserted: i_th (index - 1) = v;
count_increased: count = old count + 1;
index_increased: index = old index + 1
put_right (v: G)
-- Insert v to the right of current position.
-- (from LIST_ADAPTER)
require -- from SEQUENCIAL_CONTAINER
insertable: insertable;
not_full: not full;
not_after: not after
ensure then -- from LINEAR_CONTAINER
inserted: i_th (index + 1) = v;
count_increased: count = old count + 1;
index_unchanged: index = old index
feature -- Removal
remove
-- Remove current item.
-- (from LIST_ADAPTER)
require -- from SEQUENCIAL_CONTAINER
prunable: prunable;
not_empty: not empty;
not_off: not off
ensure then -- from LINEAR_CONTAINER
count_decreased: count = old count - 1;
index_unchanged: not off implies index = old index
wipe_out
-- Empty container.
ensure -- from SEQUENCIAL_CONTAINER
empty: empty
ensure -- from DS_CONTAINER
wipe_out: empty
feature -- Resizing
resize (n: INTEGER)
-- Resize history to n items.
-- (from LIST_ADAPTER)
require -- from SEQUENCIAL_CONTAINER
resizable: resizable;
size_increasing: n > capacity
ensure -- from SEQUENCIAL_CONTAINER
resized: capacity = n
feature -- Duplication
copy (other: like Current)
-- Copy other to list.
-- (from DS_LINKED_LIST)
require -- from GENERAL
other_not_void: other /= void;
type_identity: same_type (other)
ensure -- from GENERAL
is_equal: is_equal (other)
invariant
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
-- from LINEAR_CONTAINER
after_definition: after = (index = count + 1);
before_definition: before = (index = 0);
isfirst_definition: isfirst = (not empty and then (index = 1));
islast_definition: islast = (not empty and then (index = count));
-- from SEQUENCIAL_CONTAINER
empty_definition: empty = (count = 0);
off_definition: off = (before or after);
empty_constraint: empty implies off;
count_range: 0 <= count and count <= capacity;
-- from DS_CONTAINER
positive_count: count >= 0;
empty_definition: empty = (count = 0);
end -- class SIMPLE_LIST