Refine the specification of item and infix "@"

Proposal

Proposal for class ARRAY:

Refine the specification of features 'item' and infix "@":

   infix "@"(i: INTEGER): G
         -- Item at index `i'.
      require
         valid_index: valid_index (i)
      ensure
         definition: Result = item (i)

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

Please select one of the following:

Strongly accept the proposal
Accept the proposal
Reject the proposal
Strongly reject the proposal
Don't mind (happy either way)
Abstain (not happy either way)

History

These features were in ELKS 1995, and are implemented by all vendors.

Notes

The postcondition of infix "@" forces item and infix "@" to be redefined consistently in descendants of ARRAY.

Impact of proposed change

Low.

Result

The proposal was accepted.

votes cast at eGroups:

Accept the proposal
                sergei_ivano-@object-tools.com
                joachim.durchhol-@halstenbach.de
                manu-@eiffel.com
                franck.arnau-@omgroup.com
                genep-@sympatico.ca
                sparke-@eiffel.ie
                eric-@gobosoft.com
                tkin-@insystems.com
                xavie-@halstenbach.com
                wagne-@ti.uni-trier.de
                jweiric-@one.net
                jc-@rh.edu
                stimul-@shadow.net
                saunder-@wchat.on.ca
                kwaxe-@aha.ru

votes sent by email:

Accept the proposal:
Ulrich Windl