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