CODEWITHSUNDEEP
eiffelpost-conditions
M. Fire
M. Fire

Reputation: 127

Unknown identifiers for ensure block in Eiffel

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!

Upvotes: 0

Views: 121

Answers (2)

Alexander Kogtenkov
Alexander Kogtenkov

Reputation: 5780

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.

Upvotes: 1

user2783273
user2783273

Reputation: 91

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.

Upvotes: 1

Related Questions