Soddisfacimento del rep invariant
per prima cosa, dimostriamo che l’invariante vale per gli oggetti restituiti dai costruttori
in modo induttivo, dimostriamo che vale per tutti i metodi (produttori e modificatori)
- assumiamo che l’invariante valga per this e per tutti gli argomenti del tipo
- dimostriamo che vale quando il metodo ritorna
- per this
- per tutti gli argomenti del tipo
- per gli oggetti del tipo ritornati
induzione sul numero di invocazioni di metodi usati per produrre il valore corrente dell’oggetto
- la base dell’induzione riguarda i costruttori