Correttezza parziale per induzione

[Michele/9611]

Ciao a tutti, scrivo per via di un dubbio sorto durante l' esecuzione di un esercizio:
* ESERCIZIO 3 (Massimo 3 + 1 + 2 + 2 + 2 punti -- da consegnare a mano).
* Dato il metodo exTre con precondizione n >= 0 e postcondizione:
* r > 0 se e solo se n % 2 == 0 ,
* sviluppare, uno alla volta, i seguenti passi:
* 1) scrivere formalmente un predicato, basato su (r > 0 se e solo se n % 2 == 0),
* che permetta di dimostrare per induzione la correttezza parziale di exTre,
* 2) scrivere esplicitamente il caso base per la dimostrazione per induzione,
* 3) scrivere esplicitamente il caso induttivo per la dimostrazione per induzione,
* 4) dimostrare che il caso base della dimostrazione per induzione e' vero,
* 5) dimostrare che il caso induttivo della dimostrazione per induzione e' vero.
*/

public static int exTre(int n) {
int r = 1;
int i = 0;
while (i < n) {
r = -r;
i = i + 1;
}
return r;
}
La mia soluzione è la seguente:
1) $ P(r,n)=(r>0hArr n pari) $
2) $ P(1,0)=(1>0hArr 0 pari) $
3) $ P(1,n+1)=(1>0hArr n+1 pari) $
4) $ P(1,0)=(1>0hArr 0 pari) $
Che ha valore $ TruehArr True=True $
5) $ P(1,n+1)=(1>0hArr 0 pari) $
Assumo vero $ P(r,n)=(r>0hArr n pari) $
Se n pari allora n+1 dispari
Se n+1 dispari r=-r e, pertanto, minore di 0
allora il valore della proposizione è:
$ falsehArr false=True $
Chiedo a qualcuno di dare un' occhiata e dirmi gentilmente dove abbia sbagliato,
ringrazio anticipatamente,
Saluti

[apatriarca]

Per prima cosa hai che l'algoritmo dipende da una sola variabile \(n\) ed \(r\) è semplicemente il risultato (che va quindi riscritto in funzione di \(n\)). Questo è abbastanza importante in quanto, per il momento, non c'è alcuna dipendenza tra \(\mathrm{exTre}(n)\) e \(\mathrm{exTre}(n+1)\). La funzione parte da \(r = 1\) e ad ogni iterazione del ciclo (che viene eseguito \(n\) volte) il valore \(r\) viene scambiato con il suo opposto. In altre parole stai calcolando \((-1)^n\). I punti sono quindi:
1. \(P(n) = (-1)^n > 0 \Leftrightarrow n \mod 2 = 0.\)
2. \(P(0) = (-1)^0 > 0 \Leftrightarrow 0 \mod 2 = 0. \)
3. \( P(n) \implies P(n+1) = (-1)^{n+1} > 0 \Leftrightarrow ( n+1 ) \mod 2 = 0. \)
4. \(0\) è pari e \((-1)^0 = 1 > 0\) per cui la condizione è verificata.
5. Si ha chiaramente che \((-1)^{n+1} = -(-1)^n.\) Abbiamo quindi che, se il valore precedente era maggiore (minore) di zero e quindi \(n\) pari (dispari) per l'ipotesi induttiva, allora il successivo è minore (maggiore) di zero ed ovviamente \(n\) è dispari (pari).

[Michele/9611]

Ti ringrazio per la risposta, è tutto perfettamente chiaro!!
Saluti