[Teoria] Correttezza parziale

[Reverendo95]

Salve,
devo sostenere l'esame di programmazione 1 e a parte sulla correttezza parziale ho dei seri dubbi. Per esempio:

Dimostrare la correttezza parziale de:
1: // m contiene un qualche numero in N
2: // n contiene un qualche numero in N
3: a = m;
4: b = 0;
5: while (b < n) do
6: a = a + 1;
7: b = b + 1;
8: end while

Questo è uno dei primi esercizi forniti dal professore, il mio problema è che non so cosa fare. Cioè immagino di dover trovare un invariante di ciclo, ma come? Solo guardando il codice cosa mi fa capire di cosa stiamo parlando?
Sono sicuro sia una cosa davvero stupida e semplice per chi risponderà a questa domanda ma davvero trovo delle grosse difficoltà a impostare il ragionamento per arrivare a una soluzione.
Grazie per un eventuale risposta.

[vict85]

Non conosco questa parte della teoria dell'informatica (ho studiato matematica), ma penso che tu debba ragionare sul fatto che a e b cambiano nello stesso modo.

[Reverendo95]

"vict85":Non conosco questa parte della teoria dell'informatica (ho studiato matematica), ma penso che tu debba ragionare sul fatto che a e b cambiano nello stesso modo.

Quello sicuramente ma come traduco quello che vedo in "proprietà" per risolvere l'esercizio? Purtroppo questa parte non è spiegata al meglio in quanto riguarda un solo esercizio all'esame per questo mi vedo costretto a rompere le scatole a voi

[Reverendo95]

Provo con un altro esempio:

* Siano dati il metodo ex3, ed il seguente predicato:
* P(a,numEl) == "ex3(a, numEl) conta la quantita' di valori pari in a[0...numeEl-1]"
* Dimostrare per induzione sul valore di numEl che, per ogni array di interi a,
* ex3(a, a.length) restituisce la quantita' di valori pari in a.
*
* Sviluppare alla volta i seguenti passi:
* 1) scrivere esplicitamente il caso base per la dimostrazione per induzione,
* 2) scrivere esplicitamente il caso induttivo per la dimostrazione per induzione,
* 3) dimostrare che il caso base della dimostrazione per induzione e' vero,
* 4) dimostrare che il caso induttivo della dimostrazione per induzione e' vero.
*/

   public static int ex3(int[] a, int numEl) {
   	if (numEl == 0)
   	  return 0;
   	else 
   	   if (a[numEl - 1] % 2 == 0)
   		 return 1 + ex3(a, numEl - 1);
   	   else 
   		 return ex3(a, numEl - 1);
   }

Io l'ho risolto cosi.
Il ciclo viene ripetuto numEl volte qualunque sia l'array.

1) caso base: P(0) == 0
2) PdI: P(numEl + 1)
3) il caso base è verificate in quanto non possono esserci elementi pari o no in un array vuoto.
4) \(\displaystyle \Sigma \) n => n+1

Il 4 punto non saprei come altro scriverlo, essendo il caso base uguale a P(n) il passo induttivo è solo P(n + 1).

Può essere una soluzione corretta? Grazie ancora

[vict85]

Per il primo esercizio io mi riferivo al fatto che \(a=b+m\).

Per il secondo, vorrei far notare che il caso numEl negativo non è gestito.

[apatriarca]

Il primo punto dovrebbe essere qualcosa come
\[ P(a, 0) = \mathrm{VERO} \]
cioè
\[ \mathrm{ex3}(a, 0) = \text{valori pari in array vuoto} = 0 \]
ed è ovviamente dimostrato in quanto gestito separatamente nel primo ramo della tua selezione. Il caso base è normalmente così semplice.

Il passo induttivo è invece
\[ \forall n \geq 0. \quad P(a, n) \implies P(a, n+1) \]
cioè
\[ \forall n \geq 0. \mathrm{ex3}(a, n) = \text{valori pari in } a[0..n-1] \implies \mathrm{ex3}(a, n+1) = \text{valori pari in } a[0..n] \]
Per dimostrare questo punto osserviamo che dobbiamo valutare il secondo ramo della selezione esterna perché n+1 è maggiore di zero. A questo punto sommiamo al valore di ex3(a, n) 1 se l'ultimo valore dell'array e pari e 0 altrimenti. Ma questo valore è certamente il risultato cercato in quanto il numero di valori pari in a[0..n] è certamente uguale al numero di valori pari in a[0..n-1] più 1 se a[n] è pari e 0 altrimenti.

[Reverendo95]

Perfetto non sono ancora in grado di risolvere ogni tipo di esercizio ma inizio a capire qualcosa di più.
Grazie mille a tutti!!