work in progress | array |
Refine the specification of feature 'put'
put (v: like item; i: INTEGER) -- Replace `i'-th entry, if in index interval, by `v'. require valid_index: valid_index (i) ensure stable_lower: lower = old lower stable_upper: upper = old upper new_item: item (i) = v stable_before_i: subarray (lower, i - 1).is_equal (old subarray (lower, i - 1)) stable_after_i: subarray (i + 1, upper).is_equal (old subarray (i + 1, upper))Please select one of the following:
votes cast at eGroups:
Accept the proposal
sergei_ivano-@object-tools.com
joachim.durchhol-@halstenbach.de
manu-@eiffel.com
richie-@netlabs.net
genep-@sympatico.ca
sparke-@eiffel.ie
eric-@gobosoft.com
xavie-@halstenbach.com
kwaxe-@aha.ru
wagne-@ti.uni-trier.de
jc-@rh.edu
stimul-@shadow.net
saunder-@wchat.on.ca
franck.arnau-@omgroup.com
votes sent by email:
Accept the proposal:
Ulrich Windl