Class DS_TABLE |

    note

>     description:

>         "Data structures whose items are accessible through keys"

>     library:    "Gobo Eiffel Structure Library"
>     copyright:  "Copyright (c) 2000-2001, Eric Bezault and others"
>     license:    "MIT License"

    deferred class interface

>     DS_TABLE [G, K]

    inherit

>     DS_CONTAINER [G]

    feature {NONE} -- Initialization

>     make_default
>             -- Create an empty container.
>             -- (From DS_CONTAINER.)
>         deferred
>         ensure
>             empty: is_empty

    feature -- Access

>     infix "@", item (k: K): G
>             -- Item associated with k
>         require
>             has_k: has (k)
>         deferred

    feature -- Measurement

>     count: INTEGER
>             -- Number of items in container
>             -- (From DS_CONTAINER.)
>         deferred

    feature -- Status report

>     is_empty: BOOLEAN
>             -- Is container empty?
>             -- (From DS_CONTAINER.)

>     valid_key (k: K): BOOLEAN
>             -- Is k a valid key?
>         deferred

>     has (k: K): BOOLEAN
>             -- Is there an item associated with k?
>         deferred
>         ensure
>             valid_key: Result implies valid_key (k)

    feature -- Comparison

>     is_equal (other: like Current): BOOLEAN
>             -- Is current container equal to other?
>             -- (From GENERAL.)
>         require
>             other_not_void: other /= Void
>         deferred
>         ensure
>             consistent: standard_is_equal (other) implies Result
>             same_type: Result implies same_type (other)
>             symmetric: Result implies other.is_equal (Current)
>             same_count: Result implies count = other.count

    feature -- Duplication

>     copy (other: like Current)
>             -- Copy other to current container.
>             -- (From GENERAL.)
>         require
>             other_not_void: other /= Void
>             type_identity: same_type (other)
>         deferred
>         ensure
>             is_equal: is_equal (other)

    feature -- Element change

>     replace (v: G; k: K)
>             -- Replace item associated with k by v.
>         require
>             has_k: has (k)
>         deferred
>         ensure
>             replaced: item (k) = v
>             same_count: count = old count

>     put (v: G; k: K)
>             -- Associate v with key k.
>         require
>             valid_key: valid_key (k)
>         deferred
>         ensure
>             inserted: has (k) and then item (k) = v
>             same_count: (old has (k)) implies (count = old count)
>             one_more: (not old has (k)) implies (count = old count + 1)

>     put_new (v: G; k: K)
>             -- Associate v with key k.
>         require
>             valid_key: valid_key (k)
>             new_item: not has (k)
>         deferred
>         ensure
>             one_more: count = old count + 1
>             inserted: has (k) and then item (k) = v

>     swap (k, l: K)
>             -- Exchange items associated with k and l.
>         require
>             valid_k: has (k)
>             valid_l: has (l)
>         ensure
>             same_count: count = old count
>             new_k: item (k) = old item (l)
>             new_l: item (l) = old item (k)

    feature -- Removal

>     remove (k: K)
>             -- Remove item associated with k.
>         require
>             valid_key: valid_key (k)
>         deferred
>         ensure
>             same_count: (not old has (k)) implies (count = old count)
>             one_less: (old has (k)) implies (count = old count - 1)
>             removed: not has (k)

>     wipe_out
>             -- Remove all items from container.
>             -- (From DS_CONTAINER.)
>         deferred
>         ensure
>             wiped_out: is_empty

    invariant

>     positive_count: count >= 0
>     empty_definition: is_empty = (count = 0)
>         -- (From DS_CONTAINER.)

    end -- class DS_TABLE