It could be just
Result = across list as c some (c.item.key = key and c.item.value = value) end
But then there are several other comments on the code:
- I do not see where the property
key /= Void
is used. So it looks like it is not required. - Given that the code of
put
inserts elements of typeITEM
, the postcondition ofput
should also useacross list ... end
instead oflist.has (key, value)
. So I suspect it should be justhas (key, value)
withoutlist.
in front of it. - I do not see any point of using an auxiliary variable
flag
. The reserved variableResult
will do just fine. - All variables in Eiffel are initialized by the default values, so there is no need to assign
0
toflag
(orfalse
toResult
in a simplified version) at the beginning of a routine. - Usually there is no need to have dedicated getters in Eiffel, so normally the code
list.item.getkey
looks likelist.item.key
. - One can preemptively exit from the loop by calling
list.finish
that moves cursor to the last item of the list when a required element is found. Then afterlist.forth
the loop exit condition is satisfied and the loop terminates.