Un invariante di classe è un predicato logico che deve risultare vero per ogni istanza di una classe in determinati punti dell'esecuzione: al termine della costruzione dell’oggetto e all’ingresso/uscita di ciascun metodo pubblico. È uno strumento di specifica e verifica usato nella programmazione per contratti e, più in generale, nel ragionamento sui tipi astratti di dato.
Definizione Sia I l’insieme delle proprietà che descrivono lo stato ammissibile degli oggetti di una classe. L’invariante di classe è una formula Inv su I che deve essere vera: al termine di ogni costruttore; all’ingresso e all’uscita di ogni metodo pubblico (se nessuna eccezione lascia l’oggetto in stato non valido); dopo ogni operazione che modifica lo stato visibile dell’oggetto.
Uso e verifica Gli invarianti di classe: documentano i vincoli sullo stato interno (ad esempio “il saldo non è negativo”, “la lunghezza memorizzata coincide con il numero di elementi”); consentono prove modulari: le precondizioni e postcondizioni dei metodi sono verificate assumendo vero l’invariante; possono essere verificati in vari modi: con supporto del linguaggio (per esempio costrutti di contratto), con annotazioni formali (es. JML) o con assert e test a runtime.
Esempio minimo Esempio in pseudocodice/Java‑like: un invariante richiede che il saldo non sia mai negativo. class ContoBancario { private int saldo;
/* Invariante di classe: saldo >= 0 */
public ContoBancario(int iniziale) { if (iniziale < 0) throw new IllegalArgumentException(); saldo = iniziale;
public void deposita(int x) { if (x < 0) throw new IllegalArgumentException(); saldo += x; assert saldo >= 0; // l’invariante continua a valere
public void preleva(int x) { if (x < 0 || x > saldo) throw new IllegalArgumentException(); saldo -= x; assert saldo >= 0; // l’invariante continua a valere
Terminologia In letteratura si usa anche il termine «invariante di rappresentazione» per indicare il vincolo sullo stato interno di un tipo astratto; il concetto coincide sostanzialmente con l’invariante di classe nel contesto orientato agli oggetti.
Note
Collegamenti esterni
Categoria:Teorie dell'informatica