arrays - 配列がソートされていることを確認するための効果的な Eiffel 事後条件

Question

配列がソートされているかどうかを示すクエリを実装しました。across配列が何かを使用してソートされているかどうかを効果的にチェックする適切な事後条件を作成したいと考えています。

私はこれを次のようにしようとしました:

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

私はこのようなものを書いてみました：

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

el.forthしかし、これはクエリではなくコマンドであるため、明らかに機能しません。

どうすればこれをacross機能させることができますか、それとも何か他のことをする必要がありますか?