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

在合同设计中，必须满足两类不变式：在创建对象之后并在调用例程之后。有没有任何例子或条件，我也必须在打电话给例行公事之前做评估？在调用例程之前和之后评估不变量？

2011-06-15 Tom Sarduy

在特征调用之前可能违反类不变量。条件可能不同，我只提出最明显的：

别名。一个对象引用了参与类不变，而其他对象由第三方修改了一些其他对象：

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

回调HADNLER，由类STRUCTURE的特征iterate_over_elements执行时使一个不变违反因为handler不处于良好状态：

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

人们可以说，所有的情况都是由于软件错误和缺陷，但这正是类不变的宗旨，以对付那些包括以下情况：当发生冲突s功能调用之前。

来源

2011-06-15 09:19:47

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

回答

相关问题