.net - ルーチンを呼び出す前後の不変条件をどこで評価しますか？

Question

コントラクトによる設計では、クラス不変条件は、オブジェクトの作成後とルーチンの呼び出し後の2つの場合に満たされる必要があります。ルーチンを呼び出す前に評価を行わなければならない例や条件はありますか？

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_elementsSTRUCTUREhandler

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

すべてのケースがソフトウェアのバグや欠陥によるものであると主張することができますが、これはまさに、機能呼び出しの前に違反が発生した場合を含むケースを検出するクラス不変条件の目的です。