Esercizio su correttezza parziale di un algoritmo

[hank12]

Salve mi serve un aiuto con l'esercizio seguente:
Assumiamo che il parametro formale a abbia sempre almeno due elementi e che a.length > i >= 1.
Dimostrare che ex3 soddisfa il seguente predicato:

ex3(a,i) <==> (per ogni k. 1<=k<=i ==> a[k-1]==a[k]+1 )

1) scrivere esplicitamente il caso base P(1) per la dimostrazione per induzione,
2) scrivere esplicitamente il caso induttivo per la dimostrazione per induzione,
3) dimostrare che il caso base P(1) della dimostrazione per induzione e' vero,
4) dimostrare che il caso induttivo della dimostrazione per induzione e' vero.

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

Sono arrivato a questo punto:
Caso base:
ex3(a,1) <==> (per ogni k. 1<=k<=1 ==> a[0]==a[1]+1 )
Dimostrazione caso base:
ci possono essere due casi a) ex3(a,1)==true, b) ex3(a,1)==false.
a) ex3(a,1) <==> (per ogni k. 1<=k<=1 ==> a[0]==a[1]+1 )
****************************************true ==> true
*********true <==> true
************** true
b) ex3(a,1) <==> (per ogni k. 1<=k<=1 ==> a[0]==a[1]+1 )
*************************************** true ==> false
********false <==> false
***************true
Ora non saprei come impostare e dimostrare il passo induttivo, mi è comunque chiaro che se una chiamata al metodo restituisca false anche una sola volta allora risultato sarà false (perchè messo in AND), mentre per restituire true ogni chiamata al metodo deve ritornare true.
Fatte queste considerazione, mi serve un aiuto per impostare il passo induttivo.
Grazie
p.s scusate gli * ripetuti, mi servivano per incolonnare i valori di verità (l'editor fa un trim degli spazi).

[apatriarca]

Ma hai già praticamente descritto il ragionamento corretto per il passo induttivo. Hai due situazioni:
1. ex3(a, k) è vero e quindi per tutti i valori di i fino a k la condizione è verificata e il risultato dipende dalla condizione per k+1.
2. ex3(a, k) è falso e allora il risultato sarà falso indipendentemente dall'ultimo valore.