Eiffel отдельный объект в обеспечение заявления - PullRequest
Новая
       47

Eiffel отдельный объект в обеспечение заявления

0 голосов
/ 24 февраля 2020

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

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

Любая причина для этого I не понимаешь? 

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

1 Ответ

1 голос
/ 26 февраля 2020

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

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

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

Были изобретены отдельные инструкции только для Избегайте написания однострочных оболочек просто для вызова отдельного объекта. В остальном лучше использовать оригинальный подход S COOP с полноценными функциями с отдельными аргументами.

...