Correttezza Parziale e Ricorsione

[Michele/9611]

Salve a tutti, ho recentemente tentato di svolgere il seguente esercizio:
* ESERCIZIO 3 (Massimo 7 punti -- da consegnare a mano).
* Dimostrare per induzione su un opportuno parametro che, per ogni n >= 0
* e' vero il predicato P(n) = "exTre(2^n) == n",
* dove il metodo ricorsivo exTre e' definito da:

static int exTre(int n){
if (n > 1)
return 1 + exTre(n/2); // la divisione e' intera
else
return 0;
}
*
* Svolgere su foglio l'esercizio secondo la seguente traccia:
*
* 1) Formulare e dimostrare la base dell'induzione [1 + 2 pt]
* 2) Formulare e dimostrare il passo induttivo, mettendo in evidenza l'ipotesi induttiva [2 + 2 pt];
*/
la mia soluzione è questa:
Caso Base

$ P(0)=exTre(2^0)=0 $
che è dimostrabile semplicemente facendo una prova di esecuzione:
0>1 false
allora return 0;

Ipotesi Induttiva

$ P(n)=exTre(2^(n))=n $

Passo induttivo

$ P(n)=exTre(2^(n))=n $ $ rArr $ $ P(n+1)=exTre(2^(n+1))=n+1 $

$ P(n+1)=exTre(2^(n+1))=n+1hArr exTre(2^n*2)=n+1hArr exTre(2^n)+exTre(2)=n+1hArrexTre(2^n)=(n+1)-exTre(2) hArr exTre(2^n)=n+1-1 $ $ hArr exTre(2^n)=n $
chiedo gentilmente di dare un'occhiata e , se possibile, farmi notare eventuali errori che, essendo la prima volta che tento di usare l' induzione per la ricorsione, sono sicuro siano presenti,
ringrazio anticipatamente,
Saluti

[apatriarca]

Non mi sono chiari i tuoi passaggi. Ma per \(n > 1,\) si ha semplicemente che \(\mathrm{exTre}(x) = 1 + \mathrm{exTre}(x/2)\). Nel tuo caso avrai quindi che \(\mathrm{exTre}(2^{n+1}) = 1 + \mathrm{exTre}(2^n) = 1 + n.\) Normalmente in questi casi è sufficiente sostituire alla funzione la sua formulazione ricorsiva e tutto si incastra correttamente.

[Michele/9611]

Ti ringrazio