Pylon: a foundation library ~ User's guide (Chapter 2) -- contents | previous | next
Concrete containers are the actual implementations of the abstract data structure hierarchy which was introduced in section (see section 1.2). These containers are presented through their flat-short forms after comments regarding the implementation of each container. The flat-short form presents the public interface of a class and is derived from its source code. Most Eiffel environments provide facilities to browse the class hierarchy and produce this form and other views of the system's classes.
Some feature comments include indications regarding complexity using the classical O(x) notation , which shows how a structure should behave, in either space or execution time. This is a function with a parameter, usually named N and referring to the number of items in the container. For instance, if a feature is `O(n)', it means that its execution time is such that there exists a constantA constant may be big, so an O(n) feature will be bound by K.n but if K is big, it may still be quite slow. K such that the function f(n)=K*n gives an upper bound on the execution time. `O(1)' is for a routine whose execution time is independent of the number of items. A complexity like this is normally amortised -- that is average, some less common cases may take much longer, for instance if a structure need to be resized. Other common complexities are O(n.log(n)) which is not too bad and O(n^2) which degrades quickly for big containers.
Iterators are used mainly by lists or through other structures converted to lists. This is the flat form of P_ITERATOR. Its ancestor P_ONEWAY_ITERATOR is similar without the `backwards' features. This is a deferred class, actual iterators are internal classes created by the library when requested from a traversable container.
In general, access to item can be considered constant and fast enough so that caching the item in a local variable is not necessary except when maximum performance is really essential.
deferred class interface P_ITERATOR [G]
ancestors
P_ITERATOR [G]
P_ONEWAY_ITERATOR [G]
P_MUTATOR
indexing
cluster: pylon, iteration;
description: "Abstract two-way linear iterator";
interface: abstract, client;
feature specification
-- Iteration
last
-- Go to the last item of the container.
require
outside : outside;
deferred
ensure
done : iterable implies (not outside);
back
-- Previous item.
require
inside : not outside;
deferred
feature specification
-- Variant support
backward_variant : INTEGER
-- Backward variant for back-only loops.
deferred
feature specification
-- Copy
copy (other : like Current)
-- Cannot copy iterator.
require
other_not_void : other /= void;
type_identity : other.same_type (Current);
ensure
is_equal : is_equal (other);
feature specification
-- Access
outside : BOOLEAN
-- Is the iterator outside the container?
deferred
iterable : BOOLEAN
-- Is the associated structure iterable (not empty)?
deferred
item : G
-- Return the item at the current position.
require
inside : not outside;
deferred
feature specification
-- Synchronization
synchronize_container
-- Set the current item of the target container to be
-- the one currently pointed at by the iterator.
-- THIS METHOD DOES CHANGE THE CONTAINER STATE.
require
inside : not outside;
deferred
ensure
done : -- container current position changed
feature specification
-- Iteration
first
-- Go to first item of the container.
require
outside : outside;
deferred
ensure
done : iterable implies (not outside);
synchronize
-- Set the iterator so that the iterator current item is
-- the current item of the container. Do not change the
-- container.
require
outside : outside;
iterable : iterable;
deferred
ensure
done : not outside;
forth
-- Next item.
require
inside : not outside;
deferred
stop
-- Finish.
require
inside : not outside;
deferred
ensure
done : outside;
feature specification
-- Iterator locking
is_locked : BOOLEAN
-- Is the current iterator locked?
deferred
lock
-- Lock iterator: lock the current item into the container
-- and leave the iterator.
require
inside : not outside;
unlocked : not is_locked;
deferred
ensure
locked : is_locked;
outside : outside;
unlock
-- Unlock iterator
require
locked : is_locked;
outside : outside;
deferred
ensure
inside : not outside;
not_locked : not is_locked;
feature specification
-- Variant support
forward_variant : INTEGER
-- Forward variant for forth-only loops.
deferred
invariant
outside_locked : (not outside) implies (not is_locked);
end interface -- class P_ITERATOR
The order relation is a deferred class which is inherited in order to create a customised sort criterion.
deferred class interface P_ORDER_RELATION [G]
ancestors
P_ORDER_RELATION [G]
indexing
cluster: pylon;
description: "Order relation between two objects for sorting";
interface: abstract, inheritance;
feature specification {PUBLIC_NONE, P_CONTAINER}
-- Criterion
ordered (first, second : G) : BOOLEAN
-- Are first and second ordered? (true if first <= second)
deferred
ensure
coherent : (Result = false) implies ordered (second, first);
end interface -- class P_ORDER_RELATION
:
Two types of lists are available: a classic (two-way) linked list with the class P_LINKED_LIST, implementing the P_LIST interface; and the sequence list, P_SEQUENCE_LIST implemented with an automatically resized array, and adding the features from P_SEQUENCE in addition to the list interface.
class interface P_LINKED_LIST [G]
ancestors
P_LINKED_LIST [G]
P_LIST [G]
P_TRAVERSABLE [G]
P_ONEWAY_TRAVERSABLE [G]
P_CONTAINER [G]
P_SORTABLE [G]
P_CONTAINER [G]
P_SEARCHABLE [G, G]
P_CONTAINER [G]
indexing
cluster: pylon, container;
description: "Abstract linked structure";
interface: inheritance;
creation
make
feature specification
make
reset
-- Remove all objects from the container.
require
writable : is_writable;
ensure
done : is_empty;
feature specification
count : INTEGER
-- Number of elements in the data structure.
feature specification
-- Iteration
iterator : P_ITERATOR [G]
-- Iterator on this list.
ensure
done : Result /= void;
is_shallow_copy : -- Result /= previous Result
feature specification
-- Lock status
is_locked : BOOLEAN
-- Is current item locked?
-- Time: O(1)
require
meaningful : not is_empty;
ensure
has_locked : (Result = true) implies has_locked;
feature specification
-- Access
item : G
-- Current item.
-- Time: O(1)
require
readable : is_readable;
not_empty : not is_empty;
feature specification
-- Action
add (it : G)
-- Add an item to the end of the list.
-- Time: O(1)
require
writable : is_writable;
not_void : not is_void (it);
ensure
keep_reference : item = it;
replace (it : G)
-- Replace the current item.
-- Time: O(1)
require
writable : is_writable;
not_empty : not is_empty;
not_void : not is_void (it);
ensure
keep_reference : item = it;
insert (it : G)
-- Insert an item before the current item.
-- Time: O(1)
require
writable : is_writable;
not_empty : not is_empty;
not_void : not is_void (it);
ensure
keep_reference : item = it;
remove
-- Remove the current item.
-- Time: O(1)
require
writable : is_writable;
not_empty : not is_empty;
unlocked : not is_locked;
feature specification
-- Sorting
sort
-- Insertion sort.
-- Time: O(count^2/4) comparisons; O(count) swaps
require
has_order : has_order;
writable : is_writable;
ensure
sorted : is_sorted;
feature specification
-- Duplication
copy (other : like Current)
-- GENERAL's copy.
-- Time: O(other.count)
require
other_not_void : other /= void;
type_identity : other.same_type (Current);
ensure
is_equal : is_equal (other);
feature specification
-- Comparison
is_equal (other : like Current) : BOOLEAN
-- GENERAL's equality relation (requires covariant arguments).
-- Time: O(count)
require
other_not_void : other /= void;
ensure
consistent : standard_is_equal (other) implies Result;
same_type : Result implies same_type (other);
symmetric : Result implies other.is_equal (Current);
is_equal_list (other : P_LIST [G]) : BOOLEAN
-- Compare two lists which can be of different dynamic type.
-- Time: O(count)
require
valid : other /= void;
feature specification
-- Conversion
from_list (other : P_LIST [G])
-- Convert from another list.
-- Note: The previous contents of this list is deleted.
-- Time: O(other.count)
require
valid : other /= void;
ensure
done : is_equal_list (other);
keep_reference : -- keep copy of items.
from_array (other : ARRAY [G])
-- Convert from an ARRAY.
-- Note: The previous contents of this list is deleted.
-- Time: O(other.count)
require
valid : other /= void;
not_void : -- for_all other.item, other.item /= Void
ensure
done : other.count = count;
keep_reference : -- keep copy of items.
from_iterable (it : P_ONEWAY_ITERATOR [G])
-- Convert from a one way linear iterable container.
-- Note: The previous contents of this list is deleted.
-- Time: O("it.count")
require
valid : it /= void;
initialised : it.outside;
ensure
keep_reference : -- keep copy of items.
to_array : ARRAY [G]
-- Convert list to ARRAY.
-- Time: O(count)
ensure
done : is_empty = (Result = void);
is_shallow_copy : -- new array, old items.
feature specification
-- Concatenation
append (other : P_LIST [G])
-- Append other container to current.
-- Time: O(other.count)
require
valid : other /= void;
ensure
keep_reference : -- keep copy of items.
append_iterable (it : P_ONEWAY_ITERATOR [G])
-- Append the items from a linear iterator.
-- Time: O("it.count")
require
valid_iterator : it /= void;
initialised : it.outside;
ensure
keep_reference : -- keep copy of items.
feature specification
-- Search
equality_search (x : G)
-- Search items in the container which are equal (as defined
-- by the = operator) with 'x'.
-- Time: O(count)
require
readable : is_readable;
value_search (x : G)
-- Search items in the container which are of equal value (as defined
-- by the is_equal routine) with 'x'.
-- Time: O(count)
require
readable : is_readable;
found : BOOLEAN
-- Result of the last search operation.
found_count : INTEGER
-- Number of items found during the last search.
require
meaningful : found = true;
ensure
meaningful : Result >= 1;
feature specification
-- Sorting
is_sorted : BOOLEAN
-- Is the container sorted?
-- Time: O(target.count)
require
has_order : has_order;
ensure
empty_sorted : is_empty implies Result;
feature specification
-- Iteration
is_protected : BOOLEAN
-- Is an iterator inside the data structure?
feature specification
-- Lock status
has_locked : BOOLEAN
-- Does this container has one or more locked items?
feature specification
-- General (from P_CONTAINER)
is_writable : BOOLEAN
-- Is the structure writable?
feature specification
-- Status
is_empty : BOOLEAN
-- Is the container empty?
is_readable : BOOLEAN
-- Is the container currently readable?
feature specification
-- Output
out : STRING
-- String representation.
ensure
is_copy : -- new string
not_void : Result /= void;
feature specification
-- Utility
is_void (x : ANY) : BOOLEAN
-- Void assertion for generic parameters.
feature specification
-- Order relation
has_order : BOOLEAN
-- Does this container has an order relation defined?
set_order (ord_rel : P_ORDER_RELATION [G])
-- Set the order relation which will be used
-- when sorting. The relation stays the same when
-- the container is reset.
require
valid : ord_rel /= void;
ensure
keep_reference : has_order;
invariant
sym_current_first : (current_node = void) = (first_node = void);
sym_first_last : (first_node = void) = (last_node = void);
correct_bounds : (not is_empty) implies ((first_node.previous = void) and (last_node.next = void));
positive : count >= 0;
valid_protect_count : protcount >= 0;
protection : is_protected implies (not is_writable);
empty : is_empty = (count = 0);
end interface -- class P_LINKED_LIST
class interface P_SEQUENCE_LIST [G]
ancestors
P_SEQUENCE_LIST [G]
P_LIST [G]
P_TRAVERSABLE [G]
P_ONEWAY_TRAVERSABLE [G]
P_CONTAINER [G]
P_SORTABLE [G]
P_CONTAINER [G]
P_SEARCHABLE [G, G]
P_CONTAINER [G]
P_SEQUENCE [G]
P_CONTAINER [G]
indexing
cluster: pylon, container;
description: "Concrete indexed list, implemented by an array";
comment: "Implemented with an ARRAY whose size is doubled (and reduced) automatically";
interface: client;
creation
make
feature specification
-- Creation
make
-- Remove all items.
-- Time: O(1)
reset
-- Remove all items.
-- Time: O(1)
require
writable : is_writable;
ensure
done : is_empty;
feature specification
-- Iteration
iterator : P_ITERATOR [G]
-- Get a two-way iterator on this container.
ensure
done : Result /= void;
is_shallow_copy : -- Result /= previous Result
feature specification
-- Access
set_index (i : INTEGER)
-- Set current item to position 'i'.
-- Time: O(1)
require
not_empty : not is_empty;
index_low : i >= 1;
index_up : i <= count;
feature specification
-- Status
count : INTEGER
-- Quantity of items in the list.
item : G
-- Get current item.
-- Time: O(1)
require
readable : is_readable;
not_empty : not is_empty;
feature specification
-- Update
add (citem : G)
-- Add item at the end of the list.
-- Added item becomes current.
-- Time: O(1) amortised
require
writable : is_writable;
not_void : not is_void (citem);
ensure
in_container : container.item (count) = citem;
count_ok : count = ((old count) + 1);
keep_reference : item = citem;
replace (citem : G)
-- Replace current item.
-- Time: O(1)
require
writable : is_writable;
not_empty : not is_empty;
not_void : not is_void (citem);
ensure
keep_reference : item = citem;
insert (citem : G)
-- Insert item at current position, and push all the following items.
-- Time: O(count)
require
writable : is_writable;
not_empty : not is_empty;
not_void : not is_void (citem);
ensure
done : item = citem;
count_ok : count = ((old count) + 1);
keep_reference : item = citem;
remove
-- Remove current item.
-- Time: O(count) amortised
require
writable : is_writable;
not_empty : not is_empty;
unlocked : not is_locked;
ensure
count_ok : count = ((old count) - 1);
feature specification
-- Lock status
is_locked : BOOLEAN
-- Is current item locked?
-- Time: O(1) amortised [dictionary search]
require
meaningful : not is_empty;
ensure
has_locked : (Result = true) implies has_locked;
feature specification
-- Sorting
sort
-- Selection sort.
-- Time: O(target.count^2) comparisons; O(target.count) swaps
require
has_order : has_order;
writable : is_writable;
ensure
sorted : is_sorted;
feature specification
-- Duplication
copy (other : like Current)
-- GENERAL's copy.
-- Time: O(other.count)
require
other_not_void : other /= void;
type_identity : other.same_type (Current);
ensure
is_equal : is_equal (other);
feature specification
-- Comparison
is_equal (other : like Current) : BOOLEAN
-- GENERAL's equality relation (requires covariant arguments).
-- Time: O(count)
require
other_not_void : other /= void;
ensure
consistent : standard_is_equal (other) implies Result;
same_type : Result implies same_type (other);
symmetric : Result implies other.is_equal (Current);
is_equal_list (other : P_LIST [G]) : BOOLEAN
-- Compare two lists which can be of different dynamic type.
-- Time: O(count)
require
valid : other /= void;
feature specification
-- Conversion
from_list (other : P_LIST [G])
-- Convert from another list.
-- Note: The previous contents of this list is deleted.
-- Time: O(other.count)
require
valid : other /= void;
ensure
done : is_equal_list (other);
keep_reference : -- keep copy of items.
from_array (other : ARRAY [G])
-- Convert from an ARRAY.
-- Note: The previous contents of this list is deleted.
-- Time: O(other.count)
require
valid : other /= void;
not_void : -- for_all other.item, other.item /= Void
ensure
done : other.count = count;
keep_reference : -- keep copy of items.
from_iterable (it : P_ONEWAY_ITERATOR [G])
-- Convert from a one way linear iterable container.
-- Note: The previous contents of this list is deleted.
-- Time: O("it.count")
require
valid : it /= void;
initialised : it.outside;
ensure
keep_reference : -- keep copy of items.
to_array : ARRAY [G]
-- Convert list to ARRAY.
-- Time: O(count)
ensure
done : is_empty = (Result = void);
is_shallow_copy : -- new array, old items.
feature specification
-- Concatenation
append (other : P_LIST [G])
-- Append other container to current.
-- Time: O(other.count)
require
valid : other /= void;
ensure
keep_reference : -- keep copy of items.
append_iterable (it : P_ONEWAY_ITERATOR [G])
-- Append the items from a linear iterator.
-- Time: O("it.count")
require
valid_iterator : it /= void;
initialised : it.outside;
ensure
keep_reference : -- keep copy of items.
feature specification
-- Search
equality_search (x : G)
-- Search items in the container which are equal (as defined
-- by the = operator) with 'x'.
-- Time: O(count)
require
readable : is_readable;
value_search (x : G)
-- Search items in the container which are of equal value (as defined
-- by the is_equal routine) with 'x'.
-- Time: O(count)
require
readable : is_readable;
found : BOOLEAN
-- Result of the last search operation.
found_count : INTEGER
-- Number of items found during the last search.
require
meaningful : found = true;
ensure
meaningful : Result >= 1;
feature specification
-- Sorting
is_sorted : BOOLEAN
-- Is the container sorted?
-- Time: O(target.count)
require
has_order : has_order;
ensure
empty_sorted : is_empty implies Result;
feature specification
-- Iteration
is_protected : BOOLEAN
-- Is an iterator inside the data structure?
feature specification
-- Lock status
has_locked : BOOLEAN
-- Does this container has one or more locked items?
feature specification
-- General (from P_CONTAINER)
is_writable : BOOLEAN
-- Is the structure writable?
feature specification
-- Status
is_empty : BOOLEAN
-- Is the container empty?
is_readable : BOOLEAN
-- Is the container currently readable?
feature specification
-- Output
out : STRING
-- String representation.
ensure
is_copy : -- new string
not_void : Result /= void;
feature specification
-- Utility
is_void (x : ANY) : BOOLEAN
-- Void assertion for generic parameters.
feature specification
-- Order relation
has_order : BOOLEAN
-- Does this container has an order relation defined?
set_order (ord_rel : P_ORDER_RELATION [G])
-- Set the order relation which will be used
-- when sorting. The relation stays the same when
-- the container is reset.
require
valid : ord_rel /= void;
ensure
keep_reference : has_order;
invariant
valid_current : (not is_empty) implies ((current_item >= 1) and (current_item <= count));
good_container : container.lower = 1;
big_container : (count /= 0) implies (container.upper >= count);
small_container : (count /= 0) implies ((container.count // grow_factor) <= (default_size + count));
positive : count >= 0;
valid_protect_count : protcount >= 0;
protection : is_protected implies (not is_writable);
empty : is_empty = (count = 0);
end interface -- class P_SEQUENCE_LIST
Stacks and queues are the two dispenser type provided, both are based on a linked list.
class interface P_STACK [G]
ancestors
P_STACK [G]
P_DISPENSER [G]
P_CONTAINER [G]
indexing
cluster: pylon, container;
description: "Basic stack (FIFO) -- implemented with a linked list";
interface: client;
creation
make
feature specification
make
-- Create stack
reset
-- Create stack
require
writable : is_writable;
ensure
done : is_empty;
feature specification
-- from ANY
copy (other : like Current)
-- Update current object using fields ob object attached to `other'
-- so as to yield equal objects.
require
other_not_void : other /= void;
type_identity : other.same_type (Current);
ensure
is_equal : is_equal (other);
is_equal (other : like Current) : BOOLEAN
-- Is `other' attached to an object considered equal to `Current'?
require
other_not_void : other /= void;
ensure
consistent : standard_is_equal (other) implies Result;
same_type : Result implies same_type (other);
symmetric : Result implies other.is_equal (Current);
feature specification
-- from P_CONTAINER
count : INTEGER
-- Number of items in the container.
ensure
positive : Result >= 0;
feature specification
is_writable : BOOLEAN is ???
-- Is the container currently writable?
feature specification
item : G
-- Current item.
require
readable : is_readable;
not_empty : not is_empty;
add (it : G)
-- Add an item to the dispenser (push).
ensure
keep_reference : -- keep a copy of the item.
remove
-- Remove an item from the dispenser and update
-- the current item (pop).
require
meaningful : not is_empty;
feature specification
-- Collection interface.
to_list : P_LIST [G]
-- Items in stack (bottom of stack first).
ensure
valid_result : Result /= void;
is_shallow_copy : -- new list but old items.
feature specification
-- Status
is_empty : BOOLEAN
-- Is the container empty?
is_readable : BOOLEAN
-- Is the container currently readable?
feature specification
-- Output
out : STRING
-- String representation.
ensure
is_copy : -- new string
not_void : Result /= void;
feature specification
-- Utility
is_void (x : ANY) : BOOLEAN
-- Void assertion for generic parameters.
invariant
empty : is_empty = (count = 0);
end interface -- class P_STACK
class interface P_QUEUE [G]
ancestors
P_QUEUE [G]
P_DISPENSER [G]
P_CONTAINER [G]
indexing
cluster: pylon, container;
description: "Basic queue (LIFO) -- implemented with a linked list";
interface: client;
creation
make
feature specification
make
-- Create stack
reset
-- Create stack
require
writable : is_writable;
ensure
done : is_empty;
feature specification
-- from ANY
copy (other : like Current)
-- Update current object using fields ob object attached to `other'
-- so as to yield equal objects.
require
other_not_void : other /= void;
type_identity : other.same_type (Current);
ensure
is_equal : is_equal (other);
is_equal (other : like Current) : BOOLEAN
-- Is `other' attached to an object considered equal to `Current'?
require
other_not_void : other /= void;
ensure
consistent : standard_is_equal (other) implies Result;
same_type : Result implies same_type (other);
symmetric : Result implies other.is_equal (Current);
feature specification
-- from P_CONTAINER
count : INTEGER
-- Number of items in the container.
ensure
positive : Result >= 0;
feature specification
is_writable : BOOLEAN is ???
-- Is the container currently writable?
feature specification
item : G
-- Current item.
require
readable : is_readable;
not_empty : not is_empty;
add (it : G)
-- Add an item to the dispenser (push).
ensure
keep_reference : -- keep a copy of the item.
remove
-- Remove an item from the dispenser and update
-- the current item (pop).
require
meaningful : not is_empty;
feature specification
-- Collection interface.
to_list : P_LIST [G]
-- Items in stack (bottom of stack first).
ensure
valid_result : Result /= void;
is_shallow_copy : -- new list but old items.
feature specification
-- Status
is_empty : BOOLEAN
-- Is the container empty?
is_readable : BOOLEAN
-- Is the container currently readable?
feature specification
-- Output
out : STRING
-- String representation.
ensure
is_copy : -- new string
not_void : Result /= void;
feature specification
-- Utility
is_void (x : ANY) : BOOLEAN
-- Void assertion for generic parameters.
invariant
empty : is_empty = (count = 0);
end interface -- class P_QUEUE
The reference implementation of sets is P_HASH_SET which, as the name indicates, is implemented using a hash table. In consequence, an added constraint compared to the base P_SET is that the item type must inherit from HASHABLE.
Being based on a hash table means that search operations (or has) can be executed in constant time (assuming a good distribution of hash values). In order to maintain the average number of entries in the table under a constant, it is dynamically resized when it grows or shrinks so that some adding or removal operations may be slower when the hash table is rebuilt.
class interface P_HASH_SET [G -> HASHABLE]
ancestors
P_HASH_SET [G -> HASHABLE]
P_SET [G]
P_SEARCHABLE [G, G]
P_CONTAINER [G]
indexing
cluster: pylon, container;
description: "Set of hashable values ";
interface: client;
implementation: "Automatically resized hash table (indexed list of linked lists)";
warning: "Hash code must not change after item has been added to container";
creation
make
feature specification
-- Creation
make
-- Create set.
reset
-- Create set.
require
writable : is_writable;
ensure
done : is_empty;
feature specification
count : INTEGER
-- Number of items in the container.
is_writable : BOOLEAN is ???
-- Is the container currently writable?
feature specification
item : G
-- Current item.
-- Time: O(1)
require
readable : is_readable;
not_empty : not is_empty;
feature specification
-- Collection interface
to_list : P_LIST [G]
-- Convert the hash set to a (linked) list.
-- Time: O(count)
ensure
done : (Result /= void) and then (Result.count = count);
is_shallow_copy : -- new list, but real items
feature specification
search (x : G)
-- Search item in container (compare using is_equal).
-- Time: O(1)
require
readable : is_readable;
ensure
search_eq_has : found implies has (x);
item_set : found implies item.is_equal (x);
found : BOOLEAN
-- Result of last search.
-- Time: O(1), attribute
feature specification
has (it : G) : BOOLEAN
-- Is the item in the container (side-effect free `search')
-- Time: O(1)
feature specification
add (it : G)
-- Add item to container.
-- Time: O(1), amortised
require
writable : is_writable;
not_void : not is_void (it);
has_not : not has (it);
ensure
count : count = ((old count) + 1);
keep_reference : has (it);
remove
-- Remove current item.
-- Time: 0(1), amortised
require
writable : is_writable;
not_empty : not is_empty;
ensure
count : count = ((old count) - 1);
done : -- not has(old item)
done : -- not has(old item)
feature specification
-- General
copy (other : like Current)
-- Copy set (same items).
-- Time: 0(count)
require
other_not_void : other /= void;
type_identity : other.same_type (Current);
ensure
is_equal : is_equal (other);
is_equal (other : like Current) : BOOLEAN
-- Other container equal?
-- Time: O(count)
require
other_not_void : other /= void;
ensure
done_count : Result implies (count = other.count);
done : -- Result implies (for_each item other.has(item))
consistent : standard_is_equal (other) implies Result;
same_type : Result implies same_type (other);
symmetric : Result implies other.is_equal (Current);
feature specification
-- Search
found_count : INTEGER
-- A set has only one copy of each item.
require
meaningful : found = true;
ensure
set_count : Result = 1;
meaningful : Result >= 1;
feature specification
-- Status
is_empty : BOOLEAN
-- Is the container empty?
is_readable : BOOLEAN
-- Is the container currently readable?
feature specification
-- Output
out : STRING
-- String representation.
ensure
is_copy : -- new string
not_void : Result /= void;
feature specification
-- Utility
is_void (x : ANY) : BOOLEAN
-- Void assertion for generic parameters.
invariant
resize_up : (count // hashsize) <= (grow_entries + 1);
resize_down : ((not is_empty) and then (hashsize > default_hashsize)) implies ((count // hashsize) >= (shrink_entries - 1));
has_hashtable : hashtable /= void;
hashsize : hashsize = hashtable.count;
current_item : (not is_empty) implies (hashlist /= void);
empty : is_empty = (hashlist = void);
positive : count >= 0;
empty : is_empty = (count = 0);
end interface -- class P_HASH_SET
A dictionary, or associative array, is a table with each item associated with a unique key (in the sense of is_equal). Therefore, is_key_writable is false for a key which is already in use.
The class P_DICTIONARY uses a hash-based set to implement the dictionary (each key and item pair is a unique node in the set).
class interface P_DICTIONARY [G, K -> HASHABLE]
ancestors
P_DICTIONARY [G, K -> HASHABLE]
P_TABLE [G, K]
P_CONTAINER [G]
P_SEARCHABLE [G, K]
P_CONTAINER [G]
indexing
cluster: pylon, container;
description: "Table with one item per key";
interface: client;
creation
make
feature specification
make
-- Initialise.
reset
-- Initialise.
require
writable : is_writable;
ensure
done : is_empty;
feature specification
key_search (k : K)
-- Search key and set current item if successful.
-- is_equal is used to compare keys.
require
readable : is_readable;
found : BOOLEAN
-- Result of key search.
found_count : INTEGER is ???
-- Number of items found during the last search.
feature specification
-- from ANY
copy (other : like Current)
-- Copy.
require
other_not_void : other /= void;
type_identity : other.same_type (Current);
ensure
is_equal : is_equal (other);
is_equal (other : like Current) : BOOLEAN
-- Equality.
require
other_not_void : other /= void;
ensure
consistent : standard_is_equal (other) implies Result;
same_type : Result implies same_type (other);
symmetric : Result implies other.is_equal (Current);
feature specification
-- from P_CONTAINER
count : INTEGER
-- Number of items/keys.
ensure
positive : Result >= 0;
item : G
-- Current item.
require
readable : is_readable;
not_empty : not is_empty;
key : K
-- Current key.
require
readable : is_readable;
not_empty : not is_empty;
feature specification
is_writable : BOOLEAN is ???
-- Is the container currently writable?
is_key_writable (k : K) : BOOLEAN
-- Is the key already used?
require
valid : not is_void (k);
feature specification
add (it : G; k : K)
-- Add item and corresponding key.
-- (key must be available).
require
writable : is_writable;
not_void_key : not is_void (k);
acceptable_key : is_key_writable (k);
ensure
keep_reference : -- keep copy of item and key.
replace (it : G)
-- Replace current item (key unchanged).
require
meaningful : not is_empty;
writable : is_writable;
ensure
keep_reference : -- keep copy of item.
remove
-- Remove current item and associated key.
require
meaningful : not is_empty;
writable : is_writable;
feature specification
-- Collection interface
to_item_list : P_LIST [G]
-- List of items.
ensure
done : Result.count = count;
valid : Result /= void;
is_shallow_copy : -- new list generated each time (but real items)
to_key_list : P_LIST [K]
-- List of keys.
ensure
done : Result.count = count;
valid : Result /= void;
is_shallow_copy : -- new list generated each time (but real keys)
feature specification
-- Status
is_empty : BOOLEAN
-- Is the container empty?
is_readable : BOOLEAN
-- Is the container currently readable?
feature specification
-- Output
out : STRING
-- String representation.
ensure
is_copy : -- new string
not_void : Result /= void;
feature specification
-- Utility
is_void (x : ANY) : BOOLEAN
-- Void assertion for generic parameters.
invariant
meaningful : found_count >= 1;
empty : is_empty = (count = 0);
end interface -- class P_DICTIONARY
A catalog is a table which can contain several items associated with a single key, so is_key_writable is always true.
The class P_CATALOG makes use of a dictionary where items are lists of items associated with the key for its implementation.
class interface P_CATALOG [G, K -> HASHABLE]
ancestors
P_CATALOG [G, K -> HASHABLE]
P_TABLE [G, K]
P_CONTAINER [G]
P_SEARCHABLE [G, K]
P_CONTAINER [G]
indexing
cluster: pylon, container;
description: "Catalog (several items associated with a key)";
interface: client;
creation
make
feature specification
-- Creation
make
-- Initialise.
reset
-- Initialise.
require
writable : is_writable;
ensure
done : is_empty;
feature specification
-- from ANY
copy (other : like Current)
-- Copy from other catalog.
require
other_not_void : other /= void;
type_identity : other.same_type (Current);
ensure
is_equal : is_equal (other);
is_equal (other : like Current) : BOOLEAN
-- Equality.
require
other_not_void : other /= void;
ensure
consistent : standard_is_equal (other) implies Result;
same_type : Result implies same_type (other);
symmetric : Result implies other.is_equal (Current);
feature specification
-- from P_CONTAINER
count : INTEGER
-- Number of keys in container.
ensure
positive : Result >= 0;
is_writable : BOOLEAN is ???
-- Is the container currently writable?
item : G
-- Current item.
require
readable : is_readable;
not_empty : not is_empty;
feature specification
-- Catalog
item_list : P_LIST [G]
-- List of items associated with a single key.
require
not_empty : not is_empty;
ensure
is_shallow_copy : -- list of real items in the list.
feature specification
-- from P_TABLE
key_search (x : K)
-- Search by key, compared using is_equal.
require
readable : is_readable;
found : BOOLEAN
-- Result of search.
found_count : INTEGER
-- Number of items found corresponding to key.
require
meaningful : found = true;
ensure
meaningful : Result >= 1;
key : K
-- Current key.
require
readable : is_readable;
not_empty : not is_empty;
feature specification
is_key_writable (k : K) : BOOLEAN
-- Is it possible to add item with corresponding key?
-- (always true in catalog)
require
valid : not is_void (k);
ensure
catalog : Result = true;
add (x : G; k : K)
-- Add item with correspoding key.
require
writable : is_writable;
not_void_key : not is_void (k);
acceptable_key : is_key_writable (k);
ensure
keep_reference : -- keep copy of item and key.
replace (x : G)
-- Replace the first item in item list.
require
meaningful : not is_empty;
writable : is_writable;
ensure
keep_reference : -- keep copy of item.
remove
-- Remove current key and associated item(s).
require
meaningful : not is_empty;
writable : is_writable;
feature specification
to_key_list : P_LIST [K]
-- List of keys in the container.
ensure
valid : Result /= void;
is_shallow_copy : -- new list generated each time (but real keys)
to_item_list : P_LIST [G]
-- List of items in the containers (possibly more than keys).
ensure
valid : Result /= void;
is_shallow_copy : -- new list generated each time (but real items)
feature specification
-- Status
is_empty : BOOLEAN
-- Is the container empty?
is_readable : BOOLEAN
-- Is the container currently readable?
feature specification
-- Output
out : STRING
-- String representation.
ensure
is_copy : -- new string
not_void : Result /= void;
feature specification
-- Utility
is_void (x : ANY) : BOOLEAN
-- Void assertion for generic parameters.
invariant
empty : is_empty = (count = 0);
end interface -- class P_CATALOG