[Java] Correttezza parziale induzione su programma ricorsivo

[gianmarco.nuzzarello]

Ciao a tutti, non so se qualcuno mi può aiutare ma ho seri problemi con esercizi in cui mi chiede di dimostrare la correttezza di un determinato predicato facendo induzione. Vi posto un esercizio e se qualcuno è cosi gentile da risolverlo lo ringrazio infinitamente!!!

/* ESERCIZIO 3 (Massimo 2 + 2 + 3 + 3 punti -- da consegnare a mano).
* Sia dato il metodo ex3 qui sotto definito.
* Assumiamo che il parametro formale a abbia sempre almeno due elementi e che i>=2.
* Dimostrare che ex3 soddisfa il seguente predicato:
*
* ex3(a,i) == true <==> (per ogni k. 2= a[k-2]<=a[k-1])
*
* 1) scrivere esplicitamente il caso base P(2) per la dimostrazione per induzione, (2 punti)
* 2) scrivere esplicitamente il caso induttivo per la dimostrazione per induzione, (2 punti)
* 3) dimostrare che il caso base P(2) della dimostrazione per induzione e' vero, (3 punti)
* 4) dimostrare che il caso induttivo della dimostrazione per induzione e' vero. (3 punti)
*/

 
public static boolean ex3 (int[] a, int i) {
		if (i == 2)
			return a[0] <= a[1];
		else
			return ex3(a, i - 1) && a[i-2] <= a[i-1]; 
	}

[gianmarco.nuzzarello]

Faccio un piccolo up, capisco che non è facile rispondere..

[apatriarca]

Il problema non è che sia facile o difficile rispondere. Piuttosto che non hai mostrato alcun tentativo o interesse tu stesso nel cercare di risolverlo. Il primo punto ad esempio richiede esclusivamente di prendere la proposizione e provarla nel caso base con i uguale a 2. In questo caso è ex3(a, 2) è semplicemente a[ 0 ] <= a[ 1 ] che è esattamente quello che c'è a destra nella proposizione.

[gianmarco.nuzzarello]

Il problema è che non so scriverla "formalmente", il concetto in testa ce l'ho!

[apatriarca]

Provaci.

[EvilScript]

Ciao, ti do una breve mano a risolvere il punto (1) ed il punto (2) -- Per il resto puoi tranquillamente farlo tu

Il caso base è P(2), ovvero quando il programma ricorsivo è arrivato alla fine del suo indice con i == 2.
Scriveremo dunque: ex3(a,2) == true <==> (2 <= 2 <= i ==> a[0] <= a[1])
Per la risoluzione puoi applicare metodi logici che sicuramente da buon universitario avrai già visto.

Il caso induttivo invece è quando il contatore ricorsivo "i" è al passaggio i-1, cioè quando P(i-1) ==> P(i)
ex3(a,i-1) == true <==> (perOgni k. 2<=k<=i-1 ==> a[k_{i-1}-2] <= a[k_{i-1}-1])

Spero di esserti stato d'aiuto, buon esame!