eiffel - Eiffel のブロックを確保するための不明な識別子

Question

だから私はエッフェルプログラミングに不慣れで、特にループを書くことでensure、 a のブロックに事後条件を書くことを学ぼうとしています。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

しかし、何らかの理由で、 と の不明な識別子を取得しiますj。このエラーの原因と修正方法を知っている人はいますか? また、ブロックで使用across ... as ... all ... endする別の方法はありますか? ensureよろしくお願いします！