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