Unknown identifiers for ensure block in Eiffel

Question

So I'm new to Eiffel programming and I'm trying to learn to write postconditions in the ensure block of a feature, in particular with writing loops.

So I tried this:

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

But for some reason I get an unknown identifier for i and j. Does anyone know what causes this error and how I could fix it? Also, is there another alternative to using across ... as ... all ... end in the ensure block? Thanks so much in advance!

Answer 1

I don't know why you get a compilation error - I pasted your code and it compiles fine.

Incidentally, the Eiffel style guidelines say your comment should come AFTER the feature name and arguments, not before it.

Answer 2

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.