Class DS_LINKED_STACK |

    indexing

>     description:

>         "Stacks (Last-In, First-Out) implemented with linked cells"

>     library:    "Gobo Eiffel Structure Library"
>     author:     "Eric Bezault <ericb@gobosoft.com>"
>     copyright:  "Copyright (c) 1999-2001, Eric Bezault and others"
>     license:    "Eiffel Forum License v2 (see forum.txt)"

    class interface

>     DS_LINKED_STACK [G]

    inherit

>     DS_STACK [G]
>         DS_DISPENSER [G]
>             DS_SEARCHABLE [G]
>                 DS_CONTAINER [G]

    creation

>     make
>             -- Create an empty stack.
>             -- Use `=' as comparison criterion.
>         ensure
>             empty: is_empty

>     make_equal
>             -- Create an empty stack.
>             -- Use equal as comparison criterion.
>         ensure
>             empty: is_empty

>     make_default
>             -- Create an empty stack.
>             -- Use `=' as comparison criterion.
>             -- (From DS_CONTAINER.)
>         ensure
>             empty: is_empty

    feature -- Access

>     item: G
>             -- Item at top of stack
>             -- (From DS_DISPENSER.)
>         require
>             not_empty: not is_empty

>     equality_tester: DS_EQUALITY_TESTER [G]
>             -- Equality tester;
>             -- A void equality tester means that `='
>             -- will be used as comparison criterion.
>             -- (From DS_SEARCHABLE.)

    feature -- Measurement

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

>     occurrences (v: G): INTEGER
>             -- Number of times v appears in stack
>             -- (Use equality_tester's comparison criterion
>             -- if not void, use `=' criterion otherwise.)
>             -- (From DS_SEARCHABLE.)
>         ensure
>             positive: Result >= 0
>             has: has (v) implies Result >= 1

    feature -- Status report

>     has (v: G): BOOLEAN
>             -- Does stack include v?
>             -- (Use equality_tester's comparison criterion
>             -- if not void, use `=' criterion otherwise.)
>             -- (From DS_SEARCHABLE.)
>         ensure
>             not_empty: Result implies not is_empty

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

>     extendible (n: INTEGER): BOOLEAN
>             -- May stack be extended with n items?
>         require
>             positive_n: n >= 0
>         ensure
>             definition: Result = True

>     same_items (v, u: G): BOOLEAN
>             -- Are v and u considered equal?
>             -- (Use equality_tester's comparison criterion
>             -- if not void, use `=' criterion otherwise.)
>             -- (From DS_SEARCHABLE.)

>     same_equality_tester (other: DS_SEARCHABLE [G]): BOOLEAN
>             -- Does container use the same comparison
>             -- criterion as other?
>             -- (From DS_SEARCHABLE.)
>         require
>             other_not_void: other /= Void

>     equality_tester_settable (a_tester: like equality_tester): BOOLEAN
>             -- Can set_equality_tester be called with a_tester
>             -- as argument in current state of container?
>             -- (Default answer: True.)
>             -- (From DS_SEARCHABLE.)

    feature -- Comparison

>     is_equal (other: like Current): BOOLEAN
>             -- Is current stack equal to other?
>             -- (From GENERAL.)
>         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)
>             same_count: Result implies count = other.count

    feature -- Duplication

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

    feature -- Setting

>     set_equality_tester (a_tester: like equality_tester)
>             -- Set equality_tester to a_tester.
>             -- A void equality tester means that `='
>             -- will be used as comparison criterion.
>             -- (From DS_SEARCHABLE.)
>         require
>             equality_tester_settable: equality_tester_settable (a_tester)
>         ensure
>             equality_tester_set: equality_tester = a_tester

    feature -- Element change

>     put (v: G)
>             -- Push v on stack.
>             -- (From DS_DISPENSER.)
>         require
>             extendible: extendible (1)
>         ensure
>             one_more: count = old count + 1
>             pushed: item = v

>     force (v: G)
>             -- Push v on stack.
>             -- (From DS_DISPENSER.)
>         ensure
>             one_more: count = old count + 1
>             pushed: item = v

>     replace (v: G)
>             -- Replace top item by v.
>             -- (From DS_STACK.)
>         require
>             not_empty: not is_empty
>         ensure
>             same_count: count = old count
>             replaced: item = v

>     extend (other: DS_LINEAR [G])
>             -- Add items of other to stack.
>             -- Add other.first first, etc.
>             -- (From DS_DISPENSER.)
>         require
>             other_not_void: other /= Void
>             extendible: extendible (other.count)
>         ensure
>             new_count: count = old count + other.count

>     append (other: DS_LINEAR [G])
>             -- Add items of other to stack.
>             -- Add other.first first, etc.
>             -- (From DS_DISPENSER.)
>         require
>             other_not_void: other /= Void
>         ensure
>             new_count: count = old count + other.count

    feature -- Removal

>     remove
>             -- Remove top item from stack.
>             -- (From DS_DISPENSER.)
>         require
>             not_empty: not is_empty
>         ensure
>             one_less: count = old count - 1

>     prune (n: INTEGER)
>             -- Remove n items from stack.
>             -- (From DS_DISPENSER.)
>         require
>             valid_n: 0 <= n and n <= count
>         ensure
>             new_count: count = old count - n

>     keep (n: INTEGER)
>             -- Keep n items in stack.
>             -- (From DS_DISPENSER.)
>         require
>             valid_n: 0 <= n and n <= count
>         ensure
>             new_count: count = n

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

    invariant

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

    end -- class DS_LINKED_STACK