Invariante (informatica)

In informatica, un predicato è detto invariante per una sequenza di operazioni quando il predicato risulta vero prima e dopo dell'esecuzione della sequenza.

Sebbene i programmi per computer sono principalmente specificati in termini di cosa cambia, è ugualmente importante sapere o specificare le invarianti del programma.

La teoria di ottimizzazione dei compilatori, la metodologia di programmazione per contratto e i metodi formali per determinare la correttezza di un programma tengono conto delle invarianti.

I programmatori spesso fanno uso di asserzioni nel loro codice per rendere espliciti gli invarianti. Alcuni linguaggi ad oggetti hanno una sintassi speciale per specificare le invarianti di classe.

Voci correlate

• Logica di Hoare
• Invariante di classe

Portale Informatica: accedi alle voci di Wikipedia che trattano di informatica