Эйфелева разделить объект на оператор обеспечения

Question

Есть ли способ проверить отдельный объект, чтобы убедиться, что separate obj as l_obj заявление?

Я думаю, что логическая функция должна работать.

По какой причине я не понимаю?

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

Answer 1

На данный момент нет "отдельного выражения", аналогичного "отдельной инструкции". И, как вы упомянули, отдельные инструкции не допускаются в контексте, где ожидается только логическое выражение, в частности в постусловиях.

Даже если бы была такая конструкция, она бы не работала. Отдельный объект может изменять свое состояние между двумя последовательными отдельными инструкциями. Например, следующий код неверен:

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

Команда проверки может легко привести к нарушению утверждения в следующем сценарии выполнения:

1. Выполняется первая отдельная инструкция.
2. Какой-то другой процессор вызывает foo.put.
3. Инструкция по проверке сравнивает something до значения, установленного на шаге 2.

Если код должен гарантировать какое-то свойство отдельного объекта, его следует заключить в тело подпрограммы, а отдельный объект следует передать в качестве аргумента:

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

Отдельные инструкции были придуманы только для того, чтобы избежать написания однострочных оберток только для вызова отдельного объекта. В остальном лучше использовать оригинальный подход SCOOP с полноценными функциями с отдельными аргументами.