Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

structure.container

Class DS_RESIZABLE


Direct ancestors

DS_CONTAINER

Known direct descendants

DS_ARRAYED_LIST, DS_ARRAYED_STACK, DS_SPARSE_CONTAINER

Features

Invariants

indexing

description

Bounded data structures that can be resized

library

Gobo Eiffel Structure Library

copyright

Copyright (c) 1999, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/06/29 15:19:06 $

revision

$Revision: 1.9 $

deferred class

DS_RESIZABLE [G]

inherit

DS_CONTAINER

feature -- Measurement

capacity: INTEGER

-- Maximum number of items in container

count: INTEGER

-- Number of items in container

-- (From DS_CONTAINER)

default_capacity: INTEGER

-- Initial capacity in make_default
-- (Default value: 10)

ensure
default_capacity_positive: Result >= 0

feature -- Comparison

is_equal (other: like Current): BOOLEAN

-- Is current container equal to other?

-- (From ANY)

require
other_not_void: other /= Void
ensure
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result

feature -- Status report

is_empty: BOOLEAN

-- Is container empty?

-- (From DS_CONTAINER)

is_full: BOOLEAN

-- Is container full?

feature -- Removal

wipe_out

-- Remove all items from container.

-- (From DS_CONTAINER)

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
ensure
capacity_set: capacity = n

feature -- Duplication

cloned_object: like Current

-- Clone of current object

-- (From KL_CLONABLE)

ensure
cloned_not_void: Result /= Void
same_type: ANY_.same_types (Result, Current)
is_equal: Result.is_equal (Current)
copy (other: like Current)

-- Update current object using fields of object attached
-- to other, so as to yield equal objects.

-- (From ANY)

require
other_not_void: other /= Void
type_identity: same_type (other)
ensure
is_equal: is_equal (other)

invariant

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

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

-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

end