Request for comments: proposed ELKS 2000 ARRAY class 
Author Message
 Request for comments: proposed ELKS 2000 ARRAY class

1995, NICE published the first version of the Eiffel Library
Kernel Standard (ELKS).

It was acknowledged at the time that ELKS 1995 was a preliminary
document requiring thorough review. Although some steps towards this
were taken, no update to ELKS 1995 has yet been adopted.

During the last six months or so, NICE members have been working with
renewed vigour to update ELKS 1995. We are pleased to present here our
proposed ELKS 2000 ARRAY class.

Every part of the ARRAY class has been considered in detail, with
respect to the following goals:

1. To maximise interoperability between the different implementations
   of Eiffel.

2. To minimise the impact on existing code.

3. To minimise the work required by vendors to support the updated
   standard.

It was most definitely not a goal to achieve the best possible design.
We all knew better ways to do things, if we were starting with a
blank slate. But we realised that a significant improvement in
interoperability now would be much better than a "perfect" design
that may never be implemented.

The NICE discussions have been both extensive and intensive. We have
explored many underlying issues relating to the nature of kernel
classes in Eiffel and to the formulation of Eiffel library standards.
We have looked in detail at every feature of the class. More messages
have been exchanged about the ARRAY class in the past six months,
than about all NICE library issues in the previous eight years.

Participants in the discussions included library authors, end users,
and representatives of all Eiffel vendors. We are all very e{*filter*}d
by the possibility to achieve a truly interoperable kernel library
for Eiffel.

About the specification
=======================

For the first time, an ELKS class has been fully-specified by means
of assertions. This yields some precise but lengthy postconditions
that use recursion to assert a condition over all elements of the
ARRAY.

Please note the following points:

  - Eiffel turns off assertion checking for features called within
    an assertion, so the recursive postconditions are not fully
    executable.

  - A vendor is not required to include these assertions in
    the delivery of a conforming kernel library.

  - The complex postconditions may be rather daunting to the novice,
    and we anticipate that versions of the standard will be circulated
    in other formats too.

Three of the features are grouped together under the tag "Basic
specifiers", and have no postconditions. All other queries are
specified (directly or indirectly) in terms of these three queries.
All commands are specified by their effect on the values of these
three queries. This approach is due to James McKim, and has enabled
us to fully-specify the ARRAY class.

Request for comments
====================

We invite comments, particularly regarding the correctness and
consistency of the specification.

If you wish to comment, please do so either in the comp.lang.eiffel
newsgroup, or on the Eiffel Forum mailing list, or by joining NICE
( http://www.*-*-*.com/ ) and participating in the discussions at
http://www.*-*-*.com/

Members of NICE will be participating in these forums. If errors or
inconsistencies in the ARRAY specification come to light, the
specification will be amended before it is presented to the NICE
Board as the proposed ELKS 2000 ARRAY class.

We don't anticipate that any major design change will be necessary.
If you think a major change is needed, you may wish to search the
discussion archive at http://www.*-*-*.com/
to see the reasons behind the current design.

If you have any comments to make, please do so by 10 March 2000, or
earlier if possible.

Changes from ELKS 1995 to ELKS 2000
===================================

Remove features `make_from_array' and `to_c'.

   We could not find a way to include these features in ELKS 2000 in
   a way that was meaningful, interoperable, and readily
   implementable by all vendors. Features removed from the standard
   may still be supported by a conforming implementation, and could
   be re-introduced into a future version of the standard if the
   interoperability problems can be overcome.

Add features `is_empty', `subarray', `all_default', `same_items', and
`clear_all'.

   We considered these features to be very useful, and easy to
   implement in a way that is interoperable. Many of these features
   are already implemented outside of ELKS 1995 by one or more
   vendors. Some of these new features are particularly useful in the
   specification itself.

Refine the specifications of `is_equal', `resize', and `force'.

   There is significant divergence in the current implementations of
   these features. We have refined these specifications to make them
   rigorous. We have specified these features in a way that should
   make it as easy as possible for all vendors to implement them, and
   should cause as little disruption to existing code as possible -
   but unfortunately some disruption seems unavoidable.

Refine the specifications of `valid_index', `count', `put', `item',

   These specifications were refined to make them rigorous. Sometimes
   the specification matches what is already implemented by all
   vendors. Other times, minor changes will be needed by one or
   more vendors. However, we do not expect significant disruption
   to existing code.


features `entry' and `enter'.

   There appear to be no technical barriers to removing the frozen

   `enter' redundant. Consolidating these features yields a cleaner
   and simpler class interface.

It is not possible in this short presentation to effectively
summarise the discussions that led to these changes. If you want
to know why these changes were considered appropriate, please
browse the archive of the discussions at
http://www.*-*-*.com/

We took a consensus poll for every one of these changes. The majority
of changes gained near-unanimous or unanimous support.

Proposed ELKS 2000 ARRAY class
==============================

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

creation

   make (min_index, max_index: INTEGER)
      -- Allocate array to hold values for indexes in
      -- `min_index' .. `max_index'.
      -- Set all values to default.
      -- (Make array empty if `maxindex' = `minindex' - 1).
      require
         valid_bounds: min_index <= max_index + 1
      ensure
         lower_set: lower = min_index
         upper_set: upper = max_index
         items_set: all_default

feature -- Basic specifiers

   item (i: INTEGER): G
      -- Item at index `i'.
      require
         valid_index: valid_index (i)

   lower: INTEGER
      -- Minimum index

   upper: INTEGER
      -- Maximum index

feature -- Access


      -- Item at index `i'.
      require
         valid_index: valid_index (i)
      ensure
         definition: Result = item (i)

feature -- Measurement

   count: INTEGER
      -- Number of available indices
      ensure
         consistent_with_bounds: Result = upper - lower + 1

feature -- Comparison

   is_equal (other: like Current): BOOLEAN
      -- Do both arrays have the same `lower', `upper', and items?
      -- (Redefined from GENERAL.)
      require -- from GENERAL
         other_not_void: other /= Void
      ensure -- from GENERAL
         consistent: standard_is_equal (other) implies Result
         same_type: Result implies same_type (other)
         symmetric: Result implies other.is_equal (Current)
      ensure then
         definition: Result = (same_type (other) and then
            (lower = other.lower) and then same_items (other))

feature -- Status report

   all_default: BOOLEAN
      -- Do all items have their type's default value?
      ensure
         definition: Result = (
            count = 0 or else (
             (item(upper) = Void or else
              item(upper) = item(upper).default)
              and subarray(lower, upper - 1).all_default
            ))

   is_empty: BOOLEAN
       -- Is array empty?
       ensure
          definition: Result = (count = 0)

   same_items (other: like Current): BOOLEAN
      -- Do both arrays have the same items?
      require
         other_not_void: other /= Void
      ensure
         definition: Result =
            ((count = other.count) and then
            (count = 0 or else
            (item (upper) = other.item (other.upper) and
              subarray (lower, upper-1).same_items
               (other.subarray (other.lower, other.upper - 1)))))

   valid_index (i: INTEGER): BOOLEAN
      -- Is `i' within bounds?
      ensure
         definition: Result = ((lower <= i) and (i <= upper))

feature -- Element change

   clear_all
      -- Set every item to its default value.
      ensure
         stable_upper: upper = old upper
         stable_lower: lower = old lower
         default_items: all_default

   force (v: like item; i: INTEGER)
      -- Make `v' the item at index `i'.
      -- Always applicable: resize the array, preserving existing
      -- items, if `i' falls out of current bounds.
      ensure
         new_item: item (i) = v
         new_lower: lower = i.min (old lower)
         new_upper: upper = i.max (old upper)
         new_low_items:
            i < old lower implies
             subarray (i + 1, old lower - 1).all_default
         new_high_items:
            i > old upper implies
             subarray (old upper + 1, i - 1).all_default
         between_lower_and_i:
            subarray (old lower, ((i-1).max (old lower-1))
             .min (old upper)).same_items
             (old subarray (lower, ((i-1).max (lower-1)).min (upper)))
         between_i_and_upper:
            subarray (((i+1).min (old upper+1))
             .max (old lower), old upper).same_items
             (old subarray (((i+1).min (upper+1)).max (lower), upper))

   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:
          subarray (lower, i - 1).is_equal
             (old subarray (lower, i - 1))
         stable_after_i:
          subarray (i + 1, upper).is_equal
             (old subarray (i + 1, upper))

feature -- Resizing

   resize (min_index, max_index: INTEGER)
      -- Resize to bounds `min_index' and `max_index'.
      -- Do not lose any item whose index is in both
      -- `lower..upper' and `min_index..max_index'.
   require
      valid_bounds: min_index <= max_index + 1
   ensure
      new_lower: lower = min_index
      new_upper: upper = max_index
      default_if_too_small:
         min_index < old lower implies subarray
          (min_index, max_index.min (old lower - 1)).all_default
      default_if_too_large:
         max_index > old upper implies subarray
          (min_index.max (old upper + 1), max_index).all_default
      stable_in_intersection:
         subarray ((min_index.max (old lower)).min(old upper + 1),
            (max_index.min (old upper)).max(old lower - 1)).same_items
               (old subarray ((min_index.max (lower)).min(upper + 1),
               (max_index.min (upper)).max(lower - 1)))

feature -- Duplication

   copy (other: like Current)
      -- Reinitialize by copying all the items of `other'.
      -- (Also used by `clone'.)
      -- (Redefined from GENERAL.)
      require --from GENERAL
         other_not_void: other /= Void
         type_identity: same_type (other)
      ensure -- from GENERAL
         is_equal: is_equal (other)

    subarray (min, max: INTEGER): ARRAY [G]
       -- New array consisting of items at indexes
       -- in `min .. max'
       require
          min_large_enough: lower <= min
          max_small_enough: max <= upper
          valid_bounds: min <= max + 1
       ensure
          lower_set: Result.lower = min
          upper_set: Result.upper = max
          items_set:
             Result.count > 0 implies
                (Result.item (max) = item (max) and
                Result.subarray (min, max - 1).is_equal
                   (subarray (min, max - 1)))

invariant

   valid_bounds: lower <= upper + 1

end

--   The correctness of this specification is based on the following
--   assumptions:
--
--   1. No feature of ARRAY calls a command on any of its arguments.
--
--   2. No query of ARRAY changes the value of any basic specifier.
--
--   3. No feature of ARRAY shares internal structures in any way that
--       could lead to behaviour not deducible from this
--       specification.
--
--   4. The phrase "new ARRAY" in a header comment means a
--       newly-created ARRAY to which there is no reference other than
--       from 'result'.
--
--   5. Every type has a single default value as returned by feature
--       'default' in class GENERAL.

=== end of proposed ELKS 2000 ARRAY class ===

--

19 Eden Park Lancaster LA1 4SJ UK - Phone +44 1524 32428



Thu, 15 Aug 2002 03:00:00 GMT  
 
 [ 1 post ] 

 Relevant Pages 

1. RFC: Internationalization and the year 2000 comments requested

2. ELKS 2000 standard consequences?

3. Proposed ALLOCATABLE extensions for Fortran 2000

4. Request for SML Example Code for Using First-Class Stores and Version Array

5. RFC: Internationalization and the year 2000 comments reques

6. Comments on proposed Eiffel language changes

7. Comments on the Proposed BSI I/O Library

8. Comments on proposed Poprulebase extensions

9. Elk R1.3 documentation requested

10. PPD proposed name change, comments?

11. Year 2000 Jobs Information Request

12. Proposed re.LOCALE change: request for opinions

 

 
Powered by phpBB® Forum Software