Pylon: a foundation library ~ User's guide (Chapter 2) -- contents | previous | next


2 Data structure reference

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.

2.1 Iterators

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

2.2 Order relation

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

:

2.3 Lists

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.

2.3.1 Linked list

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

2.3.2 Sequence 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

2.4 Dispensers

Stacks and queues are the two dispenser type provided, both are based on a linked list.

2.4.1 Stack

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

2.4.2 Queue

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

2.5 Set

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

2.6 Tables

2.6.1 Dictionary

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

2.6.2 Catalog

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