Nella programmazione , un ciclo è un'istruzione che consente di ripetere l' esecuzione di una parte di un programma . Un ciclo invariante è una proprietà che è vera prima e dopo ogni ripetizione. È una proprietà logica, che consente di studiare un programma o un algoritmo .
Nella verifica formale , in particolare nella logica di Hoare , gli invarianti dei cicli sono predicati logici , che servono a dimostrare gli algoritmi che li utilizzano, in particolare la correttezza di questi algoritmi.
Un ciclo invariante deve essere vero prima di avviare il ciclo ed è quindi garantito che rimanga corretto dopo ogni iterazione del ciclo. In particolare, l'invariante sarà sempre vero alla fine del ciclo. Poiché i cicli e la ricorsione sono fondamentalmente simili, c'è poca differenza tra provare un ciclo invariante e provare che un programma è corretto usando il ragionamento di induzione . In pratica, il ciclo invariante è spesso la proprietà di induzione - l'ipotesi di induzione - che viene utilizzata per mostrare che un programma ricorsivo è equivalente a un ciclo.
Il programma C max() restituisce il valore dell'elemento più grande del suo argomento, l' array a[] , se la sua dimensione nè almeno 1.
Sulle righe 3, 6, 9, 11 e 13 del programma, un commento fornisce una proprietà in questa fase dell'esecuzione del codice. Le proprietà delle righe 6 e 11 sono letteralmente le stesse, quindi è un invariante del ciclo tra le righe 5 e 12. Quando si raggiunge la riga 13, l'invariante è ancora valida e sappiamo che la condizione i!=ndi continuazione della riga 5 è falsa; queste due proprietà implicano che msia uguale al valore massimo in a[0...n-1], quello che deve essere calcolato dalla funzione, in modo che alla riga 14 venga restituito il valore corretto.
int max(int n, const int a[]) { int m = a[0]; // m est égal à la valeur maximale de a[0...0] int i = 1; while (i != n) { // m est égal à la valeur maximale de a[0...i-1] if (m < a[i]) m = a[i]; // m est égal à la valeur maximale de a[0...i] ++i; // m est égal à la valeur maximale de a[0...i-1] } // m est égal à la valeur maximale de a[0...i-1], et i==n return m; }Se si seguisse il paradigma di programmazione difensiva , la condizione di ciclo della i!=nriga 5 dovrebbe essere i<ntale da evitare cicli infiniti per valori negativi, teoricamente proibiti di n. Anche se intuitivamente non dovrebbe fare differenza, la dimostrazione diventa un po 'più complessa in quanto i>=nè certa solo la riga 13. Per ottenere i<=nquesta condizione bisogna aggiungere l'invariante di ciclo. Rimane semplice vedere che i<=nè anche un ciclo invariante poiché la i<nlinea 6 può essere ottenuta dalla condizione di ciclo (modificata) della linea 5, e quindi che i<=nmantiene la linea 11 dopo che la linea 10 iè stata incrementata. Tuttavia, quando vengono fornite le invarianti dei cicli formalmente ai programmi di verifica, proprietà così ovvie che i<=nsono state spesso ignorate.
Il linguaggio Eiffel offre in modo nativo il supporto per le invarianti di ciclo. Gli invarianti di ciclo sono espressi con una sintassi simile a quella degli invarianti di classe . Nell'esempio seguente, l'espressione invariante del ciclo x <= 10deve essere vera dopo l'inizializzazione e quindi dopo ogni esecuzione del ciclo e ciò viene verificato in fase di esecuzione.
from x := 0 invariant x <= 10 until x >= 10 loop x := x + 1 end