1

我已经实现了一个查询，它告诉数组是否已排序。我想制作一个好的后置条件，可以有效地检查数组是否使用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工作或我应该做其他事情？

4

2 回答 2

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
于 2017-09-16T03:49:55.627 回答
1

您可以迭代索引而不是数组。像这样的东西：

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

于 2017-09-15T23:57:33.373 回答