Dove valutare gli invarianti dopo e prima di chiamare una routine?

Question

Nel design per contratti, l'invariante di classe deve essere soddisfatta in due occasioni: dopo aver creato l'oggetto e dopo aver chiamato una routine. Ci sono esempi o condizioni, che devo fare la valutazione anche prima della chiamata alla routine?

Answer 1

La classe invariante può essere violata prima di una chiamata. Le condizioni possono essere diverse, sto presentando solo quelle più ovvie:

1. Aliasing. Un oggetto fa riferimento a qualche altro oggetto coinvolto in una classe invariante e che l'altro oggetto è modificato da una terza parte:

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

   Ora il seguente codice viola l'invariante della 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. Stato esterno. Un oggetto è accoppiato a dati esterni a cui si fa riferimento in una classe invariante e può cambiare inaspettatamente:

   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
   

   Ora, se il database viene modificato al di fuori dell'applicazione, la cache può diventare incoerente e una violazione invariante di classe viene attivata prima della seguente chiamata:

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

3. Richiama. Un oggetto può essere passato all'altro in uno stato non valido:

   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 callback a HADNLER, eseguito dalla funzione iterate_over_elements della classe STRUCTURE, provoca una violazione invariante perché handler non è in buone condizioni:

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

Si può sostenere che tutti i casi sono dovuti a bug e difetti del software, ma questo è esattamente lo scopo degli invarianti di classe di catturare coloro che includono i casi in cui la violazione si verifica prima delle chiamate delle caratteristiche.