NICE-ESG-Libs Digest Sun, 10 Dec 95 Volume 1 : Issue 314
Today's Topics:
Proposal RB-2: James McKim's ARRAY class
NICE Eiffel Standards Group -- Library Committee Mailing List
To post to list:
NICE-ESG-Libs@atlanta.twr.com
To send mail to the Chairman of the committee:
NICE-ESG-Libs-chair@atlanta.twr.com
Administrative matters (sign up, unsubscribe, mail problems, etc):
NICE-ESG-Libs-request@atlanta.twr.com
Date: Sun, 10 Dec 1995 10:17:45 +0000
From: Roger Browne
Subject: Proposal RB-2: James McKim's ARRAY class
To: NICE ESG Library Committee
James McKim has invited someone from the Libraries Committee to
formally propose his ARRAY class, and I am delighted to do so.
I agree with Jim's suggestion that we use formal amendments to
address any issues with which the committee might disagree, so that
Jim's motion does not get stalled just because we might not agree
with everything in it.
Thanks Jim for all the work that you have done on this proposal.
Regards,
Roger
=====
Tag:
RB-2: James McKim's ARRAY class
Class:
ARRAY
Proposed Change:
That James McKim's ARRAY class (as appended to this message)
be adopted into the Eiffel Library Standard to supersede the current
ARRAY class.
Details:
Replace the existing Section 5.12 of ELS95 by the class
appended to this message.
Rationale:
Jim's proposal builds on the ELS95 version by including more
extensive assertions. Jim also addresses issues where existing
implementations differ.
Migration strategy:
The only potential migration difficulty identified so far is due to
differing existing implementations of 'resize'. Jim has addressed
this by proposing to replace 'resize' by two new features.
Therefore, vendors may retain their existing implementation of
'resize' as an obsolete feature, and existing code should continue
to operate as before.
=====
class ARRAY
indexing
description: "Sequences of values, all of the same type or of a conforming
one, accessible through integer indices in a contiguous interval"
class interface
ARRAY [G]
-- Basic specification set: lower, upper, item
-- Auxiliary specification set: is_equal, valid_index
creation
make (min_index, max_index: INTEGER)
-- Allocate array; set index interval to
-- min_index .. max_index; set all values to default.
require
valid_indices: min_index <= max_index + 1
ensure
lower_initialized : lower = min_index
upper_initialized: upper = max_index
items_initialized: -- for_all i, lower..upper (item(i) = Void or else item(i) = item(i).default)
make_from_array (a: ARRAY [G])
-- Initialize from the values of 'a'.
-- Useful in particular when 'a' is a manifest array.
-- Note: representation may be shared; to avoid sharing,
-- use as "make_from_array(clone( a ))"
require
a_not_void: a /= Void
ensure
lower_initialized : lower = a.lower
upper_initialized: upper = a.upper
items_initialized: -- for_all i, lower..upper (item(i) = a.item(i))
feature -- Initialization
make (min_index, max_index: INTEGER)
-- Allocate array; set index interval to
-- min_index .. max_index; set all values to default.
require
valid_indices: min_index <= max_index + 1
ensure
lower_initialized : lower = min_index
upper_initialized: upper = max_index
items_initialized: -- for_all i, lower..upper (item(i) = Void or else item(i) = item(i).default)
make_from_array (a: ARRAY [G])
-- Initialize from the values of 'a'.
-- Useful in particular when 'a' is a manifest array.
-- Note: representation may be shared; to avoid sharing,
-- use as "make_from_array(clone( a ))"
require
a_not_void: a /= Void
ensure
lower_initialized : lower = a.lower
upper_initialized: upper = a.upper
items_initialized: -- for_all i, lower..upper (item(i) = a.item(i))
feature -- Access
entry (i: INTEGER): G
-- Entry at index i.
-- (Redefinable synonym for item and infix "@".)
require
valid_index: valid_index( i )
frozen item (i: INTEGER): G
-- Entry at index i.
require
valid_index: valid_index( i )
frozen infix "@" (i: INTEGER): G
-- Entry at index i.
require
valid_index: valid_index( i )
ensure
definition: Result = item( i )
feature -- Measurement
count: INTEGER
-- Number of available indices
ensure
definition: Result = upper - lower + 1
lower: INTEGER
-- Minimum index
upper: INTEGER
-- Maximum index
feature -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is array made of the same items as other?
-- (Redefined from GENERAL.)
require else -- from GENERAL
other_not_void: other /= Void
ensure
definition: Result = (lower = other.lower) and (upper = other.upper) --and for_all i, lower..upper (item( i ) = other.item( i ))
ensure then -- from GENERAL
consistent: standard_is_equal (other) implies Result;
same_type: Result implies same_type (other);
symmetric: Result implies other.is_equal (Current)
feature -- Status report
valid_index (i: INTEGER): BOOLEAN
-- Is i within the bounds of the array?
ensure
-- Defined here as Result = (lower <= i) and (i <= upper)
-- May be redefined in descendants.
feature -- Element change
enter (v: like item; i: INTEGER)
-- Replace i-th entry, if in index interval, by v.
-- (Redefinable synonym for put.)
require
valid_index: valid_index( i )
ensure
stable_lower: lower = old lower
stable_upper: upper = old upper
new_item: item(i) = v
stable_before_i: -- for_all n, lower..(i-1) (item(n) = old item(n))
stable_after_i: -- for_all n, (i+1)..upper (item(n) = old item(n))
force (v: like item; i: INTEGER)
-- Assign item v to i-th entry.
-- Always applicable: resize the array if i falls out of
-- currently defined bounds; preserve existing items.
ensure
new_item: item (i) = v;
new_lower: lower = i.min( old lower )
new_upper: upper = i.max( old upper )
new_low_items: -- for_all n, (i+1)..(old lower-1) (item(n) = Void or else item(n) = item(n).default)
new_high_items: -- for_all n, (old upper+1)..(i-1) (item(n) = Void or else item(n) = item(n).default)
in_between: -- for_all n, old lower..old upper (i = n or else item(n) = old item(n))
frozen put (v: like item; i: INTEGER)
-- Replace i-th entry, if in index interval, by v.
require
valid_index: valid_index( i )
ensure
stable_lower: lower = old lower
stable_upper: upper = old upper
new_item: item(i) = v
stable_before_i: -- for_all n, lower..(i-1) (item(n) = old item(n))
stable_after_i: -- for_all n, (i+1)..upper (item(n) = old item(n))
feature -- Resizing
accommodate (min_index, max_index: INTEGER)
-- Resize array so that it can accommodate
-- indices down to min_index and up to max_index.
-- Do not lose any previously entered item.
ensure
new_lower: lower = min_index.min(old lower)
new_upper: upper = max_index.max(old upper)
stable_items: -- for_all i, (old lower)..(old upper) (item(i) = old item(i))
new_low_items: -- for_all i, lower..(old lower - 1) (item(i) = Void or else item(i) = item(i).default)
new_high_items: -- for_all i, (old upper + 1)..upper (item(i) = Void or else item(i) = item(i).default)
size(min_index, max_index: INTEGER)
-- Resize the array to the given indices. Do not lose
-- any item that is in the intersection of the closed
-- intervals [lower, upper] and [min_index, max_index].
require
valid_indices: min_index <= max_index
ensure
new_lower: lower = min_index
new_upper: upper = max_index
stable_items: -- for_all i, lower..upper
((old lower <= i and i <= old upper) implies item( i ) = old item( i ))
new_items: -- for_all i, lower..upper
(i < old lower or i > old_upper) implies
(item( i ) = Void or else item( i ) = item(i).default))
feature -- Conversion
to_c: POINTER
-- Address of actual sequence of values,
-- for passing to external (non-Eiffel) routines.
CONCERN: ISE would like the type of this feature be ANY. Again,
the current proposal takes no stand on this issue.
feature -- Duplication
copy (other: like Current)
-- Reinitialize by copying all the items of other.
-- (This is also used by clone.)
-- (From GENERAL.)
require else --from GENERAL
other_not_void: other /= Void
ensure then -- from GENERAL
is_equal: is_equal (other)
invariant
consistent_size: count = upper - lower + 1;
nonnegative_count: count >= 0
valid_bounds: lower <= upper + 1
item_equals_at: -- for_all i, lower..upper (item( i ) = Current @ i)
end
--
-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525
-- Everything Eiffel: compilers/libraries/publications | +44-1772-687525
|
|
