在调用例程之后和之前，在哪里评估不变量？

问题描述

| 在按合同设计时，必须在两种情况下满足类不变式：创建对象后和调用例程后。是否有示例或条件，在调用例程之前也必须进行评估？     

解决方法

        在进行功能调用之前，可以违反类不变式。条件可能有所不同，我只介绍最明显的情况： 混叠。一个对象引用了一个类不变式中涉及的另一个对象，而另一个对象则被第三方修改了：

class SWITCH -- Creation procedure is ommitted for brevity.
feature
    toggle1,toggle2: TOGGLE -- Mutually exclusive toggles.
    ...
invariant
    toggle1.is_on = not toggle2.is_on
end

现在，以下代码违反了类

SWITCH

的不变式：

switch.toggle1.turn_on -- Make `switch.toggle1.is_on = True`
switch.toggle2.turn_on -- Make `switch.toggle2.is_on = True`
switch.operate -- Class invariant is violated before this call

外部状态。对象与在类不变式中引用的外部数据耦合，并且可能会意外更改：

class TABLE_CELL feature
    item: DATA
        do
            Result := cache -- Attempt to use cached value.
            if not attached Result then
                    -- Load data from the database (slow).
                Result := database.load_item (...)
                cache := Result
            end
        end
feature {NONE} -- Storage
    cache: detachable DATA
invariant
    consistent_cache: -- Cache contains up-to-date value.
        attached cache as value implies
        value ~ database.load_item (...)
end

现在，如果在应用程序外部修改数据库，则缓存可能会变得不一致，并在以下功能调用之前触发类不变违规：

data := table_cell.item -- Class invariant is violated before this call.

打回来。可以将一个对象以无效状态传递给另一个对象：

class HANDLER feature
    process (s: STRUCTURE)
        do
            ... -- Some code that sets `is_valid` to False.
            s.iterate_over_elements (Current)
        end
    process_element (e: ELEMENT)
        do
            ...
        end
    is_valid: BOOLEAN
        do
            ...
        end
invariant
    is_valid
end

由类

STRUCTURE

的功能

iterate_over_elements

执行的对

HADNLER

的回调会导致不变的冲突，因为

handler

状况不佳：

handler.process_element (...) -- Class invariant is violated before the call.

可以说所有情况都是由于软件错误和缺陷引起的，但这正是类不变式捕获这些特征（包括在功能调用之前发生违例的情况）的目的。