Où évaluer avant et après invariants appeler une routine?

Question

Dans la conception des contrats, l'invariant de classe doit être satisfaite à deux reprises: après avoir créé l'objet et après appel d'une routine. Y a-t-il des exemples ou des conditions que je dois faire l'évaluation avant l'appel à la routine aussi?

Answer 1

L'invariant de classe peut être violée avant un appel fonction. Les conditions peuvent être différentes, je présente seulement les plus évidents:

1. Aliasing. Une des références d'objet d'un autre objet qui est impliqué dans un invariant de classe et cet autre objet est modifié par un tiers:

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

   Maintenant, le code suivant viole l'invariant de la classe 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. état externe. Un objet est couplé à des données externes qui est référencé dans un invariant de classe et peuvent changer de façon inattendue:

   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
   

   Maintenant, si la base de données est modifiée en dehors de l'application, le cache peut devenir incohérent et une violation invariant de classe est déclenchée avant l'appel de fonction suivante:

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

3. Callback. Un objet peut être transmis à l'autre dans un état non valide:

   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
   

   Un rappel à HADNLER, réalisée par la fonction iterate_over_elements de la STRUCTURE de classe, provoque une violation invariant parce handler n'est pas en bon état:

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

On peut faire valoir que tous les cas sont à cause de bogues logiciels et les défauts, mais c'est exactement le but de invariants de classe pour attraper ceux dont les cas où la violation se produit avant que les appels de fonction.