eiffel - estudio 什么时候不检查`require`？

Question

即使我在项目设置中启用了 Eiffel Studio 似乎也满足了我的要求。据我记得，我有时间在需求中设置一个断点......

我不明白我在这里缺少什么，正如您在我的示例中看到的那样，要求通过，因为我在代码上具有相同的条件并且它进入（attached {POWER_DEVICE} a_csv.device as l_dev）。

标签： eiffeldesign-by-contracteiffel-studio-19.12

Answer 1

继承断言的一般规则如下：

• 前提条件只能放宽；
• 只能加强后置条件。

在特定示例中，有效的前提条件是

    True
or else
    valid_csv (a_csv) and then attached {POWER_DEVICE} a_csv.device

require这通过特征的扁平形式中组合前置条件的开头和require else中间的关键字反映出来。表达式True是继承的。这是父项中特征的先决条件。

一个可能的解决方案是移动valid_csv (a_csv)到父特征，并valid_csv在后代中重新定义。如果valid_csv对于所有调用都是通用的，但第二个测试因后代而异，则最好引入一个新功能is_known并在父级中有 2 个前置条件子句：

is_valid_csv: is_valid_csv (a_csv)
is_known_csv: is_known_csv (a_csv)

is_known_csv类中的实现POWER_CSV_PROCESSOR将是

is_known_csv (a_csv: ...)
    do
        Result := attached {POWER_DEVICE} a_csv.device
    end

并且 feature processin的前提条件POWER_CSV_PROCESSOR是空的。

然后调用者会做类似的事情

if processor.is_known_csv (csv) then
    processor.process (csv)
end