Pagina 1 di 1

Correttezza parziale invariante di ciclo

MessaggioInviato: 07/01/2019, 14:00
da fffight
Salve, vorrei sapere se lo svolgimento di questa dimostrazione è corretta e se è sufficientemente chiara
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