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.[1][2]
Definizione
modificaSia 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.[3]
Uso e verifica
modificaGli 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.[4]
Esempio minimo
modificaEsempio 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
modificaIn 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.[4]
Note
modifica- ^ (EN) Bertrand Meyer, 11 (Design by Contract), in Object‑Oriented Software Construction, 2ª ed., Reading (MA), Addison‑Wesley, 1997, ISBN 0-13-629155-4.
- ^ (EN) Barbara Liskov e John Guttag, 5 (Representation Invariants), in Program Development in Java: Abstraction, Specification, and Object‑Oriented Design, Boston, Addison‑Wesley, 2000, ISBN 0-201-65768-6.
- ^ (EN) Bertrand Meyer, 11.7, in Object‑Oriented Software Construction, 2ª ed., Addison‑Wesley, 1997.
- ^ a b (EN) Barbara Liskov e John Guttag, 5, in Program Development in Java, Addison‑Wesley, 2000.
Collegamenti esterni
modifica- (EN) Class invariants, su Eiffel language – documentation. URL consultato il 7 novembre 2025.
- (EN) JML Reference Manual – invariants, su JML (Java Modeling Language). URL consultato il 7 novembre 2025.
