Effective Eiffel Postcondition for Ensuring that Array is sorted

Question

I have implemented a query that tells if array is sorted or not. I want to make a good postcondition that will effectively check if array is sorted using across or something else.

I tried to do this like this:

is_sorted (a: ARRAY [INTEGER]): BOOLEAN
        -- Given an array, tell if it's sorted in ascending order
    require
        array_set: a /= Void
    local
        i, j, temp: INTEGER
    do
        Result := True

        from
            i := a.lower
            j := i + 1
        invariant
            (i >= a.lower) and (i <= a.upper)
        until
            i = (a.upper) or (Result = False)
        loop
            if a[i] > a[j] then
                Result := False
            end

            i := i + 1
            j := j + 1
        variant
            a.count - i + 1
        end -- End of loop

    ensure
          -- Check if ARRAY is sorted here
    end

I tried to write something like this:

ensure
    across a as el all (el.item <= el.forth.item) end

But this obviously doesn't work because el.forth is not a query, yet a command.

How can I make this across work or should I do something else?

Answer 1

You can iterate over indexes instead of over the array. Something like that:

across 1 |..| (a.count - 1) as la_index all a.at(la_index.item) <= a.at(la_index.item + 1) end

Answer 2

To complement Louis's answer, here are some more variants. First, the same version, that takes into account that array indexes do not necessary start with 1:

across a.lower |..| (a.upper - 1) as i all a [i.item] <= a [i.item + 1] end

Unfortunately, this version does not work when upper is the minimum integer value. In this case a.upper - 1 overflows and the iteration gets a wrong integer interval. The solution is to stick to the original range of indexes, but with a condition that the last element is not compared:

across a.lower |..| a.upper as i until i.item >= a.upper all a [i.item] <= a [i.item + 1] end

Instead of iterating over an interval, the original array can be iterated directly if the last element is excluded from the comparison:

across a as i until i.target_index >= a.upper all i.item <= a [i.target_index + 1] end

or, using a dedicated query is_last:

across a as i until i.is_last all i.item <= a [i.target_index + 1] end