Salve a tutti .

Ho un problema con le invarianti di ciclo , ho meglio non riesco a capire proprio cosa sono, nelle mie dispense vengono definite così:

Invariante di ciclo = proposizione (riguardante i contenuti delle
variabili di una procedura o programma) la quale:
• è vera immediatamente prima di eseguire l'istruzione iterativa;
• è vera dopo ogni ripetizione del corpo del ciclo;
• quindi, in particolare, è vera all’uscita dall'istruzione iterativa,
cioè all'uscita "definitiva" dal ciclo.


Detto ciò io non riesco a capire che cosa devo rispondere a domande del tipo:

Scrivere l'invariante di ciclo per il seguente ciclo for:

// a e b hanno la stessa lunghezza
for (int i=0; i<a.length; i++)
b[i] = a[i];

In particolare non mi è chairo come trovare la parte sempre vera : prima dopo durante.

Secondo me la risposta era b[i]=a[i]

Ma da fonti sicure mi è stato detto che la soluzione è :

Sia n = a.length. Per tutti gli i tale che 0 <= i <= n (o n-1, se si vuole indicare la condizione di terminazione), b[i-1] = a[i-1].

Ora io non capisco perchè [i-1] e non semplicemente i

Grazie a tutti per l'attenzione,

P.S essendo un argomento di programmazione al di fuori di specifici linguaggio mi permetto di ommetere il linguaggio usato nel Titolo