Correttezza di una implementazione
invece di “eseguire” repOk (controllo dinamico), possiamo dimostrare formalmente che, ogniqualvolta un oggetto del nuovo tipo è manipolato all’esterno della classe, esso soddisfa l’invariante
- induzione sul tipo di dato
dobbiamo poi dimostrare, per ogni metodo, che l’implementazione soddisfa la specifica
- usando la funzione di rappresentazione