work in progress | array

proposals for class ARRAY

1. Refine the specification of force
2. Refine the postcondition of force

Proposal 1

Proposal for class ARRAY:

Refine the specification of feature 'force': 

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

History

This feature is implemented by all vendors.

Impact of proposed change

Low, except for VE users (when an element is forced into an empty ARRAY, the current VE behaviour is to change 'lower' and 'upper' to 'i').

Result

The proposal was accepted.

votes cast at eGroups:

Accept the proposal
                sergei_ivano-@object-tools.com
                franck.arnau-@omgroup.com
                eric-@gobosoft.com
                pete-@deakin.edu.au
                manu-@eiffel.com
                wagne-@ti.uni-trier.de
                jweiric-@one.net
                jc-@rh.edu
                saunder-@wchat.on.ca
                kwaxe-@aha.ru

votes sent by email:

Accept the proposal:
             "Ulrich Windl" <Ulrich.Windl@rz.uni-regensburg.de>

Proposal 2

Proposal for class ARRAY:

Change the postcondition of force from this: 

   ensure
      new_item: item (i) = v
      new_lower: lower = i.min (old lower)
      new_upper: upper = i.max (old upper)
      ...
...to this... 
   ensure
      new_lower: lower = i.min (old lower)
      new_upper: upper = i.max (old upper)
      new_item: item (i) = v
Please select one of the following:

Rationale

Without this change, there is no guarantee that the call to `item (i)' will have its precondition satisfied.

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
                xavie-@halstenbach.com
                kwaxe-@aha.ru
                wagne-@ti.uni-trier.de
Strongly accept the proposal
                joachim.durchhol-@halstenbach.de
                richie-@netlabs.net
                dougparde-@my-deja.com
                jweiric-@one.net
                jc-@rh.edu
                stimul-@shadow.net
                franck.arnau-@omgroup.com

votes sent by email:

Strongly accept the proposal:
                Ulrich Windl