Search code examples
eiffel

How to iterate array in precondition?

I want to iterate through array in a precondition. But It seems precondition part doesn't allow use of "from" and "across" syntax.

Is there a way to iterate through array in precondition?

insert_last (s: STRING)
require
    new_is_longer_than_prevs:
-- here I want to iterate through array "arr" and if length of s is longer than all other previously stored string values in array
do
    arr.force (s, arr.upper + 1)
end
Solution

  • The version suggested in the other reply works in most cases (it assumes the lower index of the array is 1). However, the across loop can be used directly on the array rather than on its index range:

    new_is_longer_than_prevs:
    across arr as c all s.count > c.item.count end

    This version works for any lower index and is slightly more efficient at run-time.