Capisco "invariante" nel suo senso letterale. Li riconosco anche quando digito il codice. Ma non credo di capire l'importanza di questo termine nel contesto dell'informatica.
Ogni volta che leggo conversazioni \ white paper sulla progettazione del linguaggio da famosi programmatori \ informatici, il termine 'invariante' continua a comparire come un gergo; e questa è la parte che non capisco. Cosa c'è di così speciale?
Un algoritmo è un processo ripetibile. Se è ripetibile, deve avere attributi che non cambiano con la ripetizione. Queste sono le tue invarianti. Gli invarianti sono combinati con e / o operano sui (potenzialmente) dati variabili che verranno inseriti nell'algoritmo.
Quindi l'intero punto della programmazione è identificare ciò che non varia - questo è essenzialmente il tuo programma.
Nel programma orientato agli oggetti, esiste il concetto che ogni oggetto dovrebbe fare bene una singola cosa. Ciò significa essenzialmente che (per OOP basata su classi) una classe definisce gli invarianti per un singolo algoritmo, insieme ai segnaposti (variabili) per qualsiasi variante di dati di cui potrebbero aver bisogno gli oggetti. Idealmente in OO, devi isolare ciò che varia il più possibile, in modo che ogni oggetto sia per lo più invariato.
La nozione di invariante è strongmente legata agli "effetti collaterali". Credo che sia stato promosso dall'approccio di Design by Contract (DbC) di Bertrand Meyer per la progettazione di software.
DbC arricchisce i tipi di dati astratti (backbone delle classi) con 3 nozioni importanti, precondizioni , postcondizioni, invarianti . Si spiega facilmente quando ci si riferisce alle procedure, quindi cercherò di spiegarle in riferimento:
Una precondizione rappresenta la condizione che i dati di input per una procedura devono rispettare per chiamare quella procedura. Questa precondizione deve essere rispettata e applicata dal cliente di quella particolare procedura. Il progettista di procedure potrebbe tuttavia difendere da clienti che non rispettano la condizione preliminare affermando tale condizione come prime righe nella procedura. Ad esempio avendo un metodo double divide(double dividend, double divisor) una precondizione potrebbe essere divisor != 0 .
Una postcondition rappresenta la condizione sui dati di output dopo il ritorno della procedura; è del tutto compito del progettista delle procedure rispettare questa condizione dopo aver rispettato la condizione preliminare; in uno stile di programmazione di difesa prima di tornare, la postcondizione può essere asserita.
Un invariante può essere considerato sia una precondizione che una postcondizione, ma con una comprensione diversa per la precondizione e la postcondizione dai concetti precedenti. Un invariante dice fondamentalmente che se l'input ha una condizione particolare soddisfatta prima che la procedura venisse chiamata, allora quella particolare condizione è valida dopo che la procedura è stata chiamata. Ad esempio, un invariante valido per una procedura boolean search(int term, int array[]) potrebbe dire che lo stato di array prima della chiamata è uguale a quello che è dopo la chiamata.
Applicare invarianti sulle procedure (e non solo sulle procedure) è una cosa grandiosa poiché riduce effetti collaterali ; questo è utile dal momento che gli effetti collaterali sono un grande male nella programmazione. Una particolare procedura potrebbe cambiare lo stato degli argomenti di input, oppure cambiare lo stato di alcune variabili globali o dipendere da alcune variabili globali; questo potrebbe portare a situazioni sgradevoli in cui due chiamate identiche sulla stessa procedura (con lo stesso input) potrebbero produrre output diversi. Ciò porta a conoscere la cronologia delle chiamate ed è molto difficile eseguire il debug soprattutto in un contesto di multithreading.
Un invariante è una proprietà logica che viene preservata da alcune operazioni.
Hai bisogno di invarianti per ragionare sui loop. Dato che non sai in anticipo quante iterazioni ci saranno (o non avresti bisogno di un ciclo), ogni iterazione deve preservare l'invariante, in modo che alla fine tu possa dimostrare alcune proprietà utili sul ciclo.
Hai bisogno di invarianti per ragionare sulle proprietà dei dati incapsulati. Spesso i vari dati all'interno di un modulo o di un oggetto devono soddisfare determinate proprietà per il corretto funzionamento (ad esempio, una lista che rappresenta un insieme deve essere sempre ordinata). Vuoi che ogni funzione o metodo operativo sui dati conservi queste proprietà, quindi sono anche invarianti.
Da quello che so l'importanza dell'invariant deriva dal fatto che è il mattone di base per dimostrare che un algoritmo calcola una determinata funzione. Ad esempio, hai sviluppato un nuovo algoritmo di ordinamento, ma come puoi essere sicuro che sia realmente in grado di ordinare ogni input o ogni output corretto. Il passo successivo consiste nel costruire invarianti che corrispondono al flusso dell'algoritmo e dimostrare che ordina usando gli invarianti.
Nel contesto del sistema di tipi di un linguaggio di programmazione, un tipo invariante è un tipo non convertibile. Ad esempio, in java, quando sovraccarichi un metodo, tutti i parametri sono invarianti, mentre il tipo restituito è covariante (potrebbe essere lo stesso o un sottotipo).
Leggi altre domande sui tag language-agnostic programming-languages invariants