埃菲尔铁塔中确保块的未知标识符

Question

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

所以我试了这个：

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

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

Answer 1

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

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

Answer 2

正如另一个答案中提到的，编译似乎没有问题。因此，可能需要更多信息来找出问题所在：编译器、版本等。

示例代码至少有几种替代方法：

1. 将索引迭代替换为结构本身的迭代：

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

2. 编写一个帮助程序函数，该函数将执行必要的测试并将其结果作为BOOLEAN返回。

3. 添加一个帮助程序函数，该函数循环访问结构并将测试代理作为参数，类似于

   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
   

   并通过将测试项目的代理。但是，即使它适用于单个代理，具有嵌套相互依赖代理的代码也会变得过于繁重。