Ringrazio anticipatamente e accetto volentieri consigli e suggerimenti per un miglior svolgimento di questo tipo di esercizi
* ESERCIZIO 3 (Massimo 2 + 2 + 3 + 3 punti -- da consegnare a mano).
* Sia dato il metodo e3 qui sotto definito, dove si assume che il parametro formale a contenga almeno un
* elemento. Abbreviamo con P il predicato:
*
* per ogni j <= i < a.length. a[j] <= a[i]
*
* Dimostrare per induzione sul numero di iterazioni del ciclo while che il predicato P e' invariante:
* 1) scrivere esplicitamente il caso base P 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 della dimostrazione per induzione e' vero, (3 punti)
* 4) dimostrare che il caso induttivo della dimostrazione per induzione e' vero. (3 punti)
- Codice:
public static void e3(int[] a) {
int i = 0;
while (i < a.length - 1) {
if (a[i] > a[i+1]) {
int aux = a[i];
a[i] = a[i+1];
a[i+1] = aux;
}
i++;
}
}
Svolgimento:
1) caso base P(0): per ogni j <= 0 < a.length. a[j] <= a[0], l'induzione si svolge sull'indice i
2) P(i) -> P(i+1): per ogni j <= i < a.length. a[j] <= a[i] -> per ogni j <= i + 1 < a.length. a[j] <= a[i+1]
3) dimostrazione caso base:
L'unico indice j che rientra nel range del caso base è 0 in quanto uguale a 0 <= 0 < a.length.
Il predicato quindi diventa a[0] <= a[0] che è ovviamente vero qualsiasi valore assuma a[0]
4) dimostrazione caso induttivo:
Supponiamo P(i) vero.
Il predicato al passaggio P(i+1) diventa :
per ogni j <= i + 1 < a.length. a[j] <= a[i+1]
Per ipotesi induttiva tutti i valori fino a i sono <= i
Rimangono da verificare i seguenti indici al P(i+1)
i <= i + 1
i + 1 <= i + 1 --> ma quest'ultimo è vero in quanto j = i + 1 e quindi a[j] <= a[i+1]
Rimane i <= i + 1:
Due casi (in quanto ad ogni P(i+1) c'è una condizione che può o meno verificarsi):
- Se a[i] <= a[i+1] --> la configurazione rispetta il predicato e rimane vero
- Se a[i] > a[i+1]:
Si verifica la condizione all'interno del ciclo che scambia i due valori
riportando alla configurazione a[i] <= a[i+1] che rende vero il predicato
al passaggio P(i+1)
Siccome non ci sono altri casi che possono rendere falso l'invariante, quest'ultimo è dimostrato tale