Где оценивать инварианты после и перед вызовом рутины?

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
   

   Теперь следующий код нарушает инвариант класса 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.
   

Можно утверждать, что все случаи происходят из -за ошибок и недостатков программного обеспечения, но это именно цель классовых инвариантов, чтобы поймать те, которые включая случаи, когда нарушение происходит перед вызовами функций.