Eiffel separate object into ensure statement

Question

Is there a way to have a separate object to be checked as ensure with the separate obj as l_obj statement?

I guess having a boolean function should work.

Any reason for that I don't understand?

set_position (a_pos: like position)
    do
        position := a_pos
        separate status_keeper as l_status_keeper_sep do
            l_status_keeper_sep.set_position (position)
        end
    ensure
        position = a_pos
        separate status_keeper as l_status_keeper_sep do -- the compiler doesn't agree with separate keyword here
            l_status_keeper_sep.position = a_pos
        end
    end

score 1 · Answer 1 · answered Feb 26 '20 at 00:02

At the moment there is no "separate expression" similar to "separate instruction". And, as you mention, separate instructions are not allowed in the context where only a boolean expression is expected, in postconditions in particular.

Even if there were such a construct, it would not work. The separate object could change its state between two subsequent separate instructions. For example, the following code is wrong:

separate foo as x do
    x.put (something) -- Set `foo.item` to `something`.
end
separate foo as x do
    check
        item_is_known: x.item = something
    end
end

The check instruction could easily lead to assertion violation in the following execution scenario:

The first separate instruction is executed.
Some other processor makes a call to foo.put.
The check instruction compares something to the value set in step 2.

If the code has to ensure some property of a separate object, it should be enclosed in a routine body, and the separate object should be passed as an argument:

set_position (value: like position; keeper: like status_keeper)
    do
        position := value
        keeper.set_position (value)
    ensure
        position = value
        keeper.position = value
    end

Separate instructions were invented only to avoid writing single-line wrappers just to make a call on a separate object. Anything else is better using the original SCOOP approach with full-fledged features with separate arguments.

Eiffel separate object into ensure statement

1 Answers1