work in progress | array


Class ARRAY: Changes from ELKS 2000 to ELKS 2002


September 2001:


Proposal

Proposal for class ARRAY: Add features 'make_from_array', 'array' and 'same_array' to the ELKS 2002 ARRAY class, according to the 3 SEPTEMBER 2001 version. Feature 'make_from_array' is both a creation procedure and a command.

3 SEPTEMBER 2001 VERSION:

   make_from_array (a: ARRAY [G])
      -- Initialize from the items of `a'.
      require
         a_not_void: a /= Void
      ensure
         initialized: same_array (a)

   array: ARRAY [G]
      -- New ARRAY [X] having the same items as `Current',
      -- where "X" is the result type of the `item' query.
      ensure
         array_not_void: Result /= Void
         same_count: Result.count = count
         same_indexes: Result.lower = lower
         first_item: count > 0 implies
          Result.item (lower) = item (lower)
         recurse: count > 0 implies
          Result.subarray (lower + 1, upper).is_equal (
          subarray (lower + 1, upper).array)

   same_array (other: ARRAY [G]): BOOLEAN
      -- Do `current' and `other' have the same items
      -- with the same indices?
      require
         other_not_void: other /= Void
      ensure
         definition:
            Result = array.is_equal (other.array)

Notes

These features are not present in ELKS 2000 ARRAY. Feature 'make_from_array' was present in ELKS 1995 ARRAY as a creation procedure and a command with the following specification:

   make_from_array (a: ARRAY [G])
      -- Initialize from the items of a.
      -- (Useful in proper descendants of class ARRAY,
      -- to initialize an array-like object from a manifest array.)

This feature was dropped from ELKS 2000 ARRAY because we were unable to formalise its behaviour at the time. Since then, we worked on 'make_from_string' for class STRING, and have applied the same design to this class.

These features will provide the following benefits:

   (1) within proper descendants of ARRAY, 'make_from_array' and
       'array' enable initialization of the descendant object
       from ARRAY data, and extraction of ARRAY data from
       the descendan object

   (2) 'same_array' and 'array' enable the rigorous specification
       of 'make_from_array'

   (3) 'same_array' and 'array' can be used in the assertions
       of other ARRAY features, so that those features can be
       specified in a way that is also usable in ARRAY descendants

Result

- Accept the proposal
     - gmc444@yahoo.com
     - manus@eiffel.com
     - xavier@halstenbach.com
     - franck@nenie.org
     - sparker@eiffel.ie
     - ericb@gobosoft.com
     - glennmaughan@optushome.com.au
     - berend@pobox.com
     - arno.wagner@acm.org
     - kwaxer@aha.ru
     - chris.saunders@sympatico.ca
     - peter@deakin.edu.au
     - kiniry@acm.org
- Reject the proposal
     - jeff.clark@sdrc.com

In the list discussion, it was agreed to change the header comment of 'array' to the following:

   -- New ARRAY having the same items as `Current'

...and to add the following postcondition:

      result_type: -- Result type is ARRAY [like item]


Proposal

Proposal for class ARRAY: Refine the specification of 'resize', 'force', 'is_equal' and 'subarray' to the 25 SEPTEMBER 2001 version. Add a clause to the end-of-class comments according to the 25 SEPTEMBER 2001 version.

   25 SEPTEMBER 2001 VERSION

   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)).is_equal
                  (old subarray ((min_index.max (lower)).min(upper + 1),
                  (max_index.min (upper)).max(lower - 1)))

   force (v: like item; i: INTEGER)
      -- Make `v' the item at index `i', enlarging the
      -- array if necessary.
      ensure
         new_lower: lower = i.min (old lower)
         new_upper: upper = i.max (old upper)
         new_item: item (i) = v
         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)).is_equal
             (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).is_equal
             (old subarray (((i+1).min (upper+1)).max (lower), upper))

   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
            same_array (other))

   subarray (min, max: INTEGER): like current
      -- New object 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
         subarray_not_void: Result /= Void
         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)))

   --   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. The phrase "new object" in a header comment means a
   --       newly-created object of type "like Current" to which
   --       there is no reference other than from `Result'.
   --
   --   6. Every type has a single default value as returned by feature
   --       'default' in class GENERAL.

Notes

In class ARRAY, there are five proposed changes. Here are the previous versions and the proposed chages...

1. 'resize': change postcondition

In the last postcondition, change 'same_items' to 'is_equal'.

ELKS 2000 version:

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

Suggested change:

      stable_in_intersection:
         subarray ((min_index.max (old lower)).min(old upper + 1),
            (max_index.min (old upper)).max(old lower - 1)).is_equal
               (old subarray ((min_index.max (lower)).min(upper + 1),
               (max_index.min (upper)).max(lower - 1)))

Reason: If a descendant adds new basic specifiers, and redefines 'is_equal' to take those new basic specifiers into account, the postcondition of 'resize' will automatically check that those new basic specifiers are maintained across a 'resize' operation.

2. 'force': change postcondition

In two postconditions, change 'same_items' to 'is_equal'.

ELKS 2000 version:

   force (v: like item; i: INTEGER)
      -- Make `v' the item at index `i', enlarging the
      -- array if necessary.
      ensure
         new_lower: lower = i.min (old lower)
         new_upper: upper = i.max (old upper)
         new_item: item (i) = v
         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))

Suggested change:

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

Reason for change: same as for 'resize'.

3. 'is_equal': change postcondition

Simplify the last postcondition by using 'same_array' instead of 'same_items' plus the test on 'lower'.

ELKS 2000 version:

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

Suggested change:

      ensure then
         definition: Result = (same_type (other) and then
            same_array (other))

Reason for change: The use of 'same_array' does not change the semantics, but leads to a more compact (and hopefully more readable) postcondition.

4. 'subarray': change result type and header comment

Change the result type from "ARRAY [G]" to "like current". Change the header comment from "New array..." to "New object...".

ELKS 2000 version:

   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
         subarray_not_void: Result /= Void
         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)))

Suggested change:

   subarray (min, max: INTEGER): like current
      -- New object consisting of items at indexes
      -- in `min .. max'

Reason for change: The revised signature makes this feature more likely to be useful in descendants. It is consistent with the behaviour exhibited by ELKS 2001 'substring' in descendants of STRING.

5. Add a clause to the end-of-class comments

Add a new item, numbered "5", to the end-of-class comments. Renumber the existing item "5" to item "6".

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

Suggested change:

   --   5. The phrase "new object" in a header comment means a
   --       newly-created object of type "like Current" to which
   --       there is no reference other than from `Result'.
   --
   --   6. Every type has a single default value as returned by feature
   --       'default' in class GENERAL.

Reasons for change: This parallels the ELKS 2001 STRING end-of-class comments, and clarifies the meaning of the header comment of 'subarray'.

Result

- Accept the proposal
     - ericb@gobosoft.com
     - chris.saunders@sympatico.ca
     - chcouder@club-internet.fr
     - glennmaughan@optushome.com.au
     - arno.wagner@acm.org
     - sparker@eiffel.ie
     - kwaxer@aha.ru
     - xavier@halstenbach.com
     - gmc444@yahoo.com
     - berend@pobox.com
     - James McKim (by email)


Proposal

Refine the specification of 'resize' to the 13 NOVEMBER 2001 version.

   13 NOVEMBER 2001 VERSION:

   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:
            max_index < old lower or min_index > old upper or else
             subarray (min_index.max (old lower).min (max_index + 1),
              max_index.min (old upper).max(min_index - 1)).is_equal
             (old subarray (min_index.max (lower).min(upper + 1),
              max_index.min (upper).max(lower - 1)))

The PREVIOUS version of 'resize' looks like this:

   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)).is_equal
                  (old subarray ((min_index.max (lower)).min(upper + 1),
                  (max_index.min (upper)).max(lower - 1)))

The difference between the previous version and the proposed new
version is limited to the 'stable_in_intersection' postcondition.
In the previous version, there was a bug whereby 'subarray' could
be called with invalid arguments.

In the proposed version, this bug has been fixed whilst retaining
the ability of 'resize' to work in proper descendants of class ARRAY.

Result

- Strongly accept the proposal
     - cadrian@ifrance.com
- Accept the proposal
     - kiniry@acm.org
     - manus@eiffel.com
     - Xavier.LeVourch@halstenbach.de
     - berend@pobox.com
     - chris.saunders@sympatico.ca
     - ericb@gobosoft.com
     - peter@deakin.edu.au
     - sparker@eiffel.ie
     - chcouder@club-internet.fr
     - franck@nenie.org
     - Arno Wagner (by email)
     - Alexander Kogtenkov (by email)
- Abstain (not happy either way)
     - James McKim (by email)


Proposal

Change the assertion tag of 'count' according to the 28 JANUARY 2002 version.

   28 JANUARY 2002 VERSION:

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

Notes

The tag 'consistent_with_bounds' has been changed to 'definition'.

Result

Adopted unopposed.