indexing
description: "Fixed array for WEL_STRUCTURE. Used internally by WEL."
status: "See notice at end of class."
date: "$Date$"
revision: "$Revision$"
class interface
WEL_ARRAY [G -> WEL_STRUCTURE]
create
make (a_count, an_item_size: INTEGER)
a_count
an_item_size
require
positive_count: a_count >= 0
positive_item_size: an_item_size >= 0
ensure
count_set: count = a_count
item_size_set: item_size = an_item_size
feature
item: POINTER
WEL_ANY
feature
count: INTEGER
item_size: INTEGER
structure_size: INTEGER
ensure WEL_STRUCTURE
positive_result: Result > 0
feature
exists: BOOLEAN
item
WEL_ANY
ensure WEL_ANY
Result = (item /= default_pointer)
shared: BOOLEAN
item
item
destroy_item
item
WEL_ANY
feature
set_shared
shared
WEL_ANY
ensure WEL_ANY
shared: shared
set_unshared
shared
WEL_ANY
ensure WEL_ANY
unshared: not shared
feature
i_th_item (index: INTEGER): POINTER
index
require
index_large_enough: index >= 0
index_small_enpugh: index < count
put (an_item: G; index: INTEGER)
an_itemindex
require
an_item_not_void: an_item /= void
valid_item_size: item_size = an_item.structure_size
index_large_enough: index >= 0
index_small_enough: index < count
set_item (an_item: POINTER)
iteman_item
WEL_ANY
ensure WEL_ANY
item_set: item = an_item
feature
dispose
Current
Current
WEL_ANY
feature
to_integer: INTEGER
item
WEL_ANY
ensure WEL_ANY
Result = cwel_pointer_to_integer (item)
feature
initialize
WEL_STRUCTURE
require WEL_STRUCTURE
exists: exists
initialize_with_character (a_character: CHARACTER)
a_character
WEL_STRUCTURE
require WEL_STRUCTURE
exists: exists
memory_copy (source_pointer: POINTER; length: INTEGER)
lengthsource_pointeritem
WEL_STRUCTURE
require WEL_STRUCTURE
length_small_enough: length <= structure_size
length_large_enough: length > 0
exists: exists
invariant
positive_count: count >= 0
positive_item_size: item_size >= 0
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- WEL_ARRAY