0

所以我是 Eiffel 编程的新手，我正在尝试学习在ensurea 的块中编写后置条件feature，特别是编写循环。

所以我尝试了这个：

feature
        -- sets the value of a particular in an array to x
    foo (a: ARRAY[INTEGER]; target_val, x: INTEGER)
        require
            valid_target: 1 <= target_val and target_val <= a.count  
        do
            a[target_val] := x
        ensure
            across
                1 |..| a.count as i
            all
                across
                    1 |..| a.count as j
                all
                    i.item /= j.item implies a[i.item] /= a[j.item]
                end
             end
end

但由于某种原因，我得到了一个未知标识符iand j。有谁知道导致此错误的原因以及我该如何解决？across ... as ... all ... end另外，在ensure块中使用还有另一种选择吗？提前非常感谢！

4

2 回答 2

1

As mentioned in another answer, there seems to be no issues with compilation. So, some more information may be required to figure out what's wrong: compiler, its version, etc.

There are at least several alternatives to the example code:

  1. Replace iteration over indexes with iteration over structures themselves:

    across a as u all
    across a as v all
        u.target_index /= v.target_index implies u.item /= v.item
    end
end

  2. Write a helper function that will do the necessary tests and return their results as a BOOLEAN.

  3. Add a helper function that iterates over the structure and takes an test agent as an argument, similar to

    for_all_with_index (a: ARRAY [BAR]; test: FUNCTION [BAR, INTEGER, BOOLEAN]): BOOLEAN
    do
        Result := across a as c all test (c.item, c.target_index) end
    end

    and pass agents that will test items. However, even if it works nice with a single agent, the code with nested mutually dependent agents becomes too heavy.

于 2018-09-15T15:52:37.263 回答
1

我不知道你为什么会收到编译错误 - 我粘贴了你的代码，它编译得很好。

顺便说一句，Eiffel 风格指南说您的评论应该出现在功能名称和参数之后，而不是之前。

于 2018-09-15T06:04:30.917 回答