Refine the specification of copy

Proposal

Proposal for class ARRAY:

Refine the specification of feature 'copy'

   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)

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

This feature was in ELKS 1995, and is implemented by all vendors.

Issues

Some people are not happy with the 'type_identity' precondition inherited from class GENERAL - but it's pretty much forced on us by the 'is_equal' postcondition also inherited from class GENERAL.

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
                sparke-@eiffel.ie
                franck.arnau-@omgroup.com
                genep-@sympatico.ca
                stimul-@shadow.net
                eric-@gobosoft.com
                tkin-@insystems.com
                xavie-@halstenbach.com
                wagne-@ti.uni-trier.de
                jweiric-@one.net
                jc-@rh.edu
                gmc33-@my-deja.com
                saunder-@wchat.on.ca
                kwaxe-@aha.ru

votes sent by email:

Accept the proposal:
Ulrich Windl