work in progress | array

proposals for class ARRAY

1. Add feature subarray
2. Refine the specification of subarray

Proposal 1

Proposal for class ARRAY:

Add feature 'subarray': 

   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:
            count > 0 implies
               (Result.item (max) = item (max) and
               Result.subarray (min, max - 1).is_equal
                  (subarray (min, max - 1)))

History

This feature is already implemented by HACT and ISE. Equivalent features are implemented in SmallEiffel under the names sub_array and slice.

Impact of proposed change

Low.

SmallEiffel may continue to support sub_array and slice. Alternatively, SmallEiffel may declare those features obsolete.

Result

The proposal was accepted.

votes cast at eGroups:

Strongly accept the proposal
                genepi@sympatico.ca
                richieb@netlabs.net
Accept the proposal
                sergei_ivanov@object-tools.com
                jcm@mstr.hgc.edu
                manus@eiffel.com
                peter@deakin.edu.au
                joachim.durchholz@halstenbach.de
                tking@insystems.com
                sparker@eiffel.ie
                ericb@gobosoft.com
                xavier@halstenbach.com
                kwaxer@aha.ru
                jweirich@one.net
                avt@aha.ru
                franck.arnaud@omgroup.com

votes sent by email:

Abstain:
                "Ulrich Windl" <ulrich.windl@rz.uni-regensburg.de>

Amendment

Alexander Kogtenkov pointed out that the subexpression "count > 0" (in the postcondition) should be "Result.count > 0". Jim McKim prefers to use 'min' and 'max' instead of 'Result.count'. A vote showed a preference for "Result.count > 0" as follows:

votes cast at eGroups:

Prefer "Result.count > 0"
                sparker@eiffel.ie
                ericb@gobosoft.com
                manus@eiffel.com
                joachim.durchholz@halstenbach.de
                jweirich@one.net
Don't mind (happy either way)
                genepi@sympatico.ca
                sergei_ivanov@object-tools.com
                kwaxer@aha.ru
Prefer "min <= max"
                kevin@ethossoft.co.nz
                wagner@ti.uni-trier.de
                franck.arnaud@omgroup.com

votes sent by email:

Prefer "Result.count > 0":
                "Ulrich Windl" <ulrich.windl@rz.uni-regensburg.de>

Proposal 2

Proposal for class ARRAY:

Change the postcondition of `subarray' from this: 

   ensure
      lower_set: Result.lower = min
      upper_set: Result.upper = max
      ...
...to this... 
   ensure
      subarray_not_void: Result /= Void
      lower_set: Result.lower = min
      upper_set: Result.upper = max
      ...
Please select one of the following:

Rationale

Without the postcondition subarray_not_void, we cannot guarantee that the other postconditions will not make a call on a void target.

Result

The proposal was accepted.

votes cast at eGroups:

Accept the proposal
                sergei_ivano-@object-tools.com
                manu-@eiffel.com
                gmc33-@my-deja.com
                todd.kin-@nexthr.com
                genep-@sympatico.ca
                sparke-@eiffel.ie
                simonwillcock-@enterprise.net
                kwaxe-@aha.ru
                wagne-@ti.uni-trier.de
Strongly accept the proposal
                joachim.durchhol-@halstenbach.de
                richie-@netlabs.net
                dougparde-@my-deja.com
                xavie-@halstenbach.com
                jweiric-@one.net
                jc-@rh.edu
                stimul-@shadow.net
                franck.arnau-@omgroup.com

votes sent by email:

Strongly accept the proposal:
                Ulrich Windl