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

Question

在契约式设计中，类不变量必须在两种情况下满足：创建对象之后和调用例程之后。是否有任何示例或条件，我也必须在调用例程之前进行评估？

Answer 1

在功能调用之前可以违反类不变量。条件可能不同，我只介绍最明显的条件：

1. 别名。对象引用类不变量中涉及的某个其他对象，并且该其他对象被第三方修改：

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

   现在下面的代码违反了 class 的不变量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
   

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

   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.
   

3. 打回来。一个对象可以在无效状态下传递给另一个对象：

   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由iterate_over_elements类的功能执行的对 的回调STRUCTURE会导致不变量违反，因为handler状态不佳：

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

可以争辩说，所有情况都是由于软件错误和缺陷造成的，但这正是类不变量的目的，以捕获包括违规发生在功能调用之前的情况。