0

有没有办法让一个单独的对象被检查为确保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
4

1 回答 1

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 方法会更好。

于 2020-02-26T00:02:00.007 回答