Class DS_RESIZABLE |

    indexing

>     description:

>         "Bounded data structures that can be resized"

>     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)"

    deferred class interface

>     DS_RESIZABLE [G]

    inherit

>     DS_CONTAINER [G]

    feature {NONE} -- Initialization

>     make_default
>             -- Create an empty container and allocate memory
>             -- space for at least default_capacity items.
>             -- (From DS_CONTAINER.)
>         deferred
>         ensure
>             empty: is_empty
>             capacity_set: capacity = default_capacity

    feature -- Measurement

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

>     capacity: INTEGER
>             -- Maximum number of items in container
>         deferred

>     default_capacity: INTEGER
>             -- Initial capacity in make_default
>             -- (Default value: 10)
>         ensure
>             default_capacity_positive: Result >= 0

    feature -- Status report

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

>     is_full: BOOLEAN
>             -- Is container full?

    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 -- Removal

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

    feature -- Resizing

>     resize (n: INTEGER)
>             -- Resize container so that it can contain
>             -- at least n items. Do not lose any item.
>         require
>             n_large_enough: n >= capacity
>         deferred
>         ensure
>             capacity_set: capacity = n

    invariant

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

>     count_constraint: count <= capacity
>     full_definition: is_full = (count = capacity)

    end -- class DS_RESIZABLE