Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

structure.list

Class DS_ARRAYED_LIST_CURSOR


Direct ancestors

DS_LIST_CURSOR

Creation

Features

Invariants

indexing

description

Cursors for arrayed list traversals

library

Gobo Eiffel Structure Library

copyright

Copyright (c) 1999-2001, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/07/13 17:52:13 $

revision

$Revision: 1.7 $

class

DS_ARRAYED_LIST_CURSOR [G]

inherit

DS_LIST_CURSOR

create

make (a_list: like container)

-- Create a new cursor for a_list.

require
a_list_not_void: a_list /= Void
ensure
container_set: container = a_list
before: before

feature -- Access

any_: KL_ANY_ROUTINES

-- Routines that ought to be in class ANY

-- (From KL_IMPORTED_ANY_ROUTINES)

ensure
any_routines_not_void: Result /= Void
container: DS_ARRAYED_LIST [G]

-- List traversed

-- (From DS_CURSOR)

index: INTEGER

-- Index of current position

-- (From DS_INDEXED_CURSOR)

ensure
valid_index: valid_index (Result)
item: G

-- Item at cursor position

-- (From DS_CURSOR)

require
not_off: not off

feature -- Comparison

is_equal (other: like Current): BOOLEAN

-- Are other and current cursor at the same position?

-- (From ANY)

require
other_not_void: other /= Void
ensure
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result

feature -- Status report

after: BOOLEAN

-- Is there no valid position to right of cursor?

-- (From DS_LINEAR_CURSOR)

before: BOOLEAN

-- Is there no valid position to left of cursor?

-- (From DS_BILINEAR_CURSOR)

is_first: BOOLEAN

-- Is cursor on first item?

-- (From DS_LINEAR_CURSOR)

ensure
not_empty: Result implies not container.is_empty
not_off: Result implies not off
is_last: BOOLEAN

-- Is cursor on last item?

-- (From DS_BILINEAR_CURSOR)

ensure
not_empty: Result implies not container.is_empty
not_off: Result implies not off
is_valid: BOOLEAN

-- Is cursor valid?

-- (From DS_CURSOR)

obsolete

Backward compatibility with Gobo 1.4

ensure
definition: Result = True
off: BOOLEAN

-- Is there no item at cursor position?

-- (From DS_CURSOR)

same_position (other: like Current): BOOLEAN

-- Is current cursor at same position as other?

-- (From DS_CURSOR)

require
other_not_void: other /= Void
valid_cursor (other: like Current): BOOLEAN

-- Is other a valid cursor according
-- to current traversal strategy?

-- (From DS_CURSOR)

require
other_not_void: other /= Void
ensure
Result implies container.valid_cursor (other)
valid_index (i: INTEGER): BOOLEAN

-- Is i a valid index value?

-- (From DS_INDEXED_CURSOR)

ensure then
i_large_enough: Result implies (i >= 0)
i_small_enough: Result implies (i <= (container.count + 1))

feature -- Cursor movement

back

-- Move cursor to previous position.

-- (From DS_BILINEAR_CURSOR)

require
not_before: not before
finish

-- Move cursor to last position.

-- (From DS_BILINEAR_CURSOR)

ensure
empty_behavior: container.is_empty implies before
last_or_before: is_last xor before
forth

-- Move cursor to next position.

-- (From DS_LINEAR_CURSOR)

require
not_after: not after
go_after

-- Move cursor to after position.

-- (From DS_LINEAR_CURSOR)

ensure
after: after
go_before

-- Move cursor to before position.

-- (From DS_BILINEAR_CURSOR)

ensure
before: before
go_i_th (i: INTEGER)

-- Move cursor to i-th position.

-- (From DS_INDEXED_CURSOR)

require
valid_index: valid_index (i)
ensure
moved: index = i
go_to (other: like Current)

-- Move cursor to other's position.

-- (From DS_CURSOR)

require
other_not_void: other /= Void
other_valid: valid_cursor (other)
ensure
same_position: same_position (other)
search_back (v: G)

-- Move to first position at or before current
-- position where item and v are equal.
-- (Use equality_tester's criterion from container
-- if not void, use = criterion otherwise.)
-- Move before if not found.

-- (From DS_BILINEAR_CURSOR)

require
not_off: not off or before
search_forth (v: G)

-- Move to first position at or after current
-- position where item and v are equal.
-- (Use equality_tester's criterion from container
-- if not void, use = criterion otherwise.)
-- Move after if not found.

-- (From DS_LINEAR_CURSOR)

require
not_off: not off or after
start

-- Move cursor to first position.

-- (From DS_LINEAR_CURSOR)

ensure
empty_behavior: container.is_empty implies after
first_or_after: is_first xor after

feature -- Element change

append_left (other: DS_LINEAR [G])

-- Add items of other to left of cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST_CURSOR)

require
other_not_void: other /= Void
not_before: not before
ensure
new_count: container.count = old container.count + old other.count
append_right (other: DS_LINEAR [G])

-- Add items of other to right of cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST_CURSOR)

require
other_not_void: other /= Void
not_after: not after
ensure
new_count: container.count = old container.count + old other.count
extend_left (other: DS_LINEAR [G])

-- Add items of other to left of cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST_CURSOR)

require
other_not_void: other /= Void
extendible: container.extendible (other.count)
not_before: not before
ensure
new_count: container.count = old container.count + old other.count
extend_right (other: DS_LINEAR [G])

-- Add items of other to right of cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST_CURSOR)

require
other_not_void: other /= Void
extendible: container.extendible (other.count)
not_after: not after
ensure
new_count: container.count = old container.count + old other.count
force_left (v: G)

-- Add v to left of cursor position.
-- Do not move cursors.

-- (From DS_LIST_CURSOR)

require
not_before: not before
ensure
one_more: container.count = old container.count + 1
force_right (v: G)

-- Add v to right of cursor position.
-- Do not move cursors.

-- (From DS_LIST_CURSOR)

require
not_after: not after
ensure
one_more: container.count = old container.count + 1
put_left (v: G)

-- Add v to left of cursor position.
-- Do not move cursors.

-- (From DS_LIST_CURSOR)

require
extendible: container.extendible (1)
not_before: not before
ensure
one_more: container.count = old container.count + 1
put_right (v: G)

-- Add v to right of cursor position.
-- Do not move cursors.

-- (From DS_LIST_CURSOR)

require
extendible: container.extendible (1)
not_after: not after
ensure
one_more: container.count = old container.count + 1
replace (v: G)

-- Replace item at cursor position by v.
-- (Performance: O(1).)

-- (From DS_DYNAMIC_CURSOR)

require
not_off: not off
ensure
replaced: item = v
swap (other: DS_DYNAMIC_CURSOR [G])

-- Exchange items at current and other's positions.
-- Note: cursors may reference two different containers.

-- (From DS_DYNAMIC_CURSOR)

require
not_off: not off
other_not_void: other /= Void
other_not_off: not other.off
ensure
new_item: item = old (other.item)
new_other: other.item = old item

feature -- Removal

prune_left (n: INTEGER)

-- Remove n items to left of cursor position.
-- Move all cursors off.

-- (From DS_LIST_CURSOR)

require
valid_n: 0 <= n and n < index
ensure
new_count: container.count = old container.count - n
prune_right (n: INTEGER)

-- Remove n items to right of cursor position.
-- Move all cursors off.

-- (From DS_LIST_CURSOR)

require
valid_n: 0 <= n and n <= (container.count - index)
ensure
new_count: container.count = old container.count - n
remove

-- Remove item at cursor position.
-- Move any cursors at this position forth.

-- (From DS_LIST_CURSOR)

require
not_off: not off
ensure
one_less: container.count = old container.count - 1
remove_left

-- Remove item to left of cursor position.
-- Move any cursors at this position forth.

-- (From DS_LIST_CURSOR)

require
not_empty: not container.is_empty
not_before: not before
not_first: not is_first
ensure
one_less: container.count = old container.count - 1
remove_right

-- Remove item to right of cursor position.
-- Move any cursors at this position forth.

-- (From DS_LIST_CURSOR)

require
not_empty: not container.is_empty
not_after: not after
not_last: not is_last
ensure
one_less: container.count = old container.count - 1

feature -- Duplication

copy (other: like Current)

-- Copy other to current cursor.

-- (From ANY)

require
other_not_void: other /= Void
type_identity: same_type (other)
ensure
is_equal: is_equal (other)

feature {DS_ARRAYED_LIST} -- Implementation

next_cursor: DS_ARRAYED_LIST_CURSOR [G]

-- Next cursor
-- (Used by container to keep track of traversing
-- cursors (i.e. cursors associated with container
-- and which are not currently off).)

-- (From DS_CURSOR)

position: INTEGER

-- Internal position in list

set_after

-- Set position to after position.

ensure
after: after
set_before

-- Set position to before position.

ensure
before: before
set_next_cursor (a_cursor: like next_cursor)

-- Set next_cursor to a_cursor.

-- (From DS_CURSOR)

ensure
next_cursor_set: next_cursor = a_cursor
set_position (i: INTEGER)

-- Set position to i.

require
valid_i: valid_position (i)
ensure
position_set: position = i
valid_position (p: INTEGER): BOOLEAN

-- Is p a valid value for position?

ensure
not_off: (1 <= p and p <= container.count) implies Result
before: (p = 0) implies Result
after: (p = container.after_position) implies Result

invariant


not_both: not (after and before)
before_constraint: before implies off

after_constraint: after implies off

-- From DS_CURSOR
container_not_void: container /= Void
empty_constraint: container.is_empty implies off

-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

end