[*] Invariante di ciclo

[Frapper]

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

[alka]

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

Era meglio se specificavi che la discussione era indipendente dal linguaggio con [*].

[Frapper]

Nessuno mi può aiutare?

[Habanero]

Originariamente inviato da Frapper
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

probabilmente perchè quando esci dal dal ciclo i==a.length (è il valore di i che fa terminare il ciclo) e per quel valore di i a b[i] non viene assegnato a[i]

[Frapper]

si ma quanto i vale 0 i-1 vale -1 , e -1 non è un indice valido, oppure mi sfugge qualcosa?