repOK
può essere usato da programmi di test per verificare se una implementazione preserva l’invariante
può essere usato dentro le implementazioni di costruttori e metodi
- creatori, modificatori e produttori dovrebbero chiamarlo prima di ritornare per assicurarsi che per l’oggetto costruito o modificato vale l’invariante
- per esempio, dovrebbero chiamarlo insert e remove di IntSet, add, mul, minus di Poly
se l’invariante non vale si dovrebbe sollevare FailureException