Where evaluate invariants after and before call a routine?

Question

In the design by contracts, the class invariant must be satisfied on two occasions: after creating the object and after call a routine. Are there any examples or conditions, which I have to do the evaluation before the call to the routine too?

Answer 1

The class invariant can be violated before a feature call. The conditions may be different, I'm presenting only the most obvious ones:

1. Aliasing. An object references some other object that is involved in a class invariant and that other object is modified by a third party:

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

   Now the following code violates the invariant of 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. External state. An object is coupled with external data that is referenced in a class invariant and may change unexpectedly:

   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
   

   Now if the database is modified outside the application, the cache may become inconsistent and a class invariant violation is triggered before the following feature call:

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

3. Callback. An object can be passed to the other one in an invalid state:

   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
   

   A callback to HADNLER, performed by the feature iterate_over_elements of the class STRUCTURE, causes an invariant violation because handler is not in a good condition:

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

One can argue that all the cases are because of software bugs and flaws, but this is exactly the purpose of class invariants to catch those including the cases when the violation happens before feature calls.