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

kernel.spec.ise

Class KL_SPECIAL_ROUTINES



Features

Invariants

indexing

description

Routines that ought to be in class SPECIAL. %
%A special object is a zero-based indexed sequence of values, %
%equipped with features put, item and count.

library

Gobo Eiffel Kernel Library

copyright

Copyright (c) 2003, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2004/12/22 22:47:13 $

revision

$Revision: 1.4 $

class

KL_SPECIAL_ROUTINES [G]

feature -- Initialization

make (n: INTEGER): SPECIAL [G]

-- Create a new special object being able to contain n items.

require
non_negative_n: n >= 0
ensure
special_not_void: Result /= Void
count_set: Result.count = n
make_from_array (an_array: ARRAY [G]): SPECIAL [G]

-- Create a new special object with items from an_array.

require
an_array_not_void: an_array /= Void
ensure
special_not_void: Result /= Void
count_set: Result.count = an_array.count

feature -- Status report

has (an_array: SPECIAL [G]; v: G): BOOLEAN

-- Does v appear in an_array?

require
an_array_not_void: an_array /= Void

feature -- Removal

clear_all (an_array: SPECIAL [G])

-- Reset all items to default values.

obsolete

[040930] Use `an_array.clear_all instead.

require
an_array_not_void: an_array /= Void

feature -- Resizing

resize (an_array: SPECIAL [G]; n: INTEGER): SPECIAL [G]

-- Resize an_array so that it contains n items.
-- Do not lose any previously entered items.
-- Note: the returned special object might be an_array
-- or a newly created special object where items from
-- an_array have been copied to.

require
an_array_not_void: an_array /= Void
n_large_enough: n >= an_array.count
ensure
special_not_void: Result /= Void
count_set: Result.count = n

feature -- Conversion

to_special (an_array: ARRAY [G]): SPECIAL [G]

-- Fixed array filled with items from an_array.
-- The fixed array and an_array may share
-- internal data and/or an_array may be altered.
-- Use make_from_array if this is a concern.

require
an_array_not_void: an_array /= Void
ensure
special_not_void: Result /= Void
count_set: Result.count >= an_array.count

invariant

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

end