Эффективное Эйфелево постусловие для гарантии сортировки массива

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 работать или мне делать что-то еще?

Answer 1

Вы можете перебирать индексы, а не массивы. Что-то вроде того:

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

Answer 2

Чтобы дополнить ответ Луи, вот еще несколько вариантов. Во-первых, та же версия, которая учитывает, что индексы массива не обязательно начинаются с 1:

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

К сожалению, эта версия не работает, когда upper минимальное целочисленное значение. В этом случае a.upper - 1 переполняется, и итерация получает неправильный целочисленный интервал. Решение состоит в том, чтобы придерживаться исходного диапазона индексов, но с условием, что последний элемент не сравнивается:

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

Вместо итерации по интервалу, исходный массив может быть повторен напрямую, если последний элемент исключен из сравнения:

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

или, используя специальный запрос is_last:

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