Correttezza e Terminazione (Appunti) PDF

Correttezza (e terminazione) March 3, 2021 Obiettivi: introdurre l'analisi qualitativa degli algoritmi, basata su tecniche di verica come induzione e invarianti Argomenti: i bug, correttezza (totale e parziale), verica, pre- e postcondizi...

Correttezza (e terminazione) March 3, 2021 Obiettivi: introdurre l'analisi qualitativa degli algoritmi, basata su tecniche di verica come induzione e invarianti Argomenti: i bug, correttezza (totale e parziale), verica, pre- e postcondizioni, induzione (semplice e completa), verica di algoritmi ricorsivi con induzione, invarianti di ciclo, verica di algoritmi con invarianti di ciclo, terminazione. 1 Bug, correttezza, verica, pre- e postcondizioni I bug, termine inventato da Edison, sono inevitabili: It has been just so in all of my inventions. The rst step is an intuition, and comes with a burst, then diculties arise  this thing gives out and [it is] then that "Bugs"  as such little faults and diculties are called  show themselves and months of intense watching, study and labor are requisite before commercial success or failure is certainly reached. (T. Edison, da Wikipedia) Le loro conseguenze possono essere devastanti: 1962: la sonda Mariner 1 si schianta su Venere per un errore nel software di controllo del volo 1981: una TV nel Quebec decreta la vittoria alle elezioni di un partito sconosciuto; usavano un software difettoso per la rilevazione dei risultati 1983: un sistema computerizzato sovietico rileva un attacco nucleare con cinque missili balistici inesistenti 1985: alcuni pazienti vengono irradiati con dosi eccessive di raggi X dal sistema Therac-25 a controllo software 1993: il processore Pentium, che incorpora il coprocessore aritmetico, sbaglia le divisioni in virgola mobile 1996: l'Ariane 5 esce dalla sua rotta e viene distrutto in volo a causa di un errore di conversione dei dati da 16 a 32 bit 1999: usando un nuovo sistema, le poste inglesi recapitano mezzo milione di nuovi passaporti ad indirizzi sbagliati o inesistenti 1999: Y2K è il celeberrimo millenium-bug (continua... ) Bisogna vericare la correttezza degli algoritmi (e i programmi che li implementano). Un algoritmo è corretto se per ogni input fornisce l'output corretto (correttezza totale). Un algoritmo è parzialmente corretto se per ogni input se termina fornisce l'output corretto. Un vericatore ideale, dato un problema P a un algoritmo A, dovrebbe essere in grado di rispondere:  SI, A è corretto per P oppure  NO, A non è corretto per P e gli errori sono.... Tale vericatore non esiste ma ci sono tanti progetti di ricerca che puntano a sviluppare strumenti per aiutare la verica di algoritmi e programmi. Vericare un algoritmo vuole dire controllare se esso soddisfa le speciche del problema computazionale che deve risolvere. Le speciche sono descritte tramite le precondizioni e le postcondizioni. Per esempio, per il problema della divisione intera: Precondizioni: a ≥ 0, b > 0 numeri interi; Postcondizioni: il risultato è un intero q tale che a=b·q+r con 0 ≤ r < b. 1 2 Induzione semplice e completa Schema dell'induzione semplice : Sia P (n) una enunciato che dipende da una variabile intera n ∈ N. Se P (n) vale per n = 0 e per ogni n ∈ N vale P (n) =⇒ P (n + 1) allora P (n) vale per ogni n ∈ N. Cioè ( P (0) ∧ (∀n ∈ N.P (n) =⇒ P (n + 1)) ) =⇒ ∀n ∈ N.P (n) dove P (0) è il caso base e (∀n ∈ N.P (n) =⇒ P (n + 1)) è il passo induttivo. Inoltre, P (n) viene chiamata l'ipotesi induttiva. In parole: una proprietà P (n) che vale per n=0 (caso base) e se vale per n allora vale per n+1 (passo induttivo) vale per ogni n ≥ 0. Il caso base può essere anche P (k): ( P (k) ∧ (∀n ≥ k.P (n) =⇒ P (n + 1)) ) =⇒ ∀n ≥ k.P (n) quindi la proprietà vale da k in poi. Il passo induttivo può essere anche nella forma P (n − 1) =⇒ P (n). Esempio: dimostriamo con induzione che n X (2k − 1) = n2 (1) k=1 Caso base: la proprietà con n=1 vale 1 X (2k − 1) = 1 = 12 k=1 Passo induttivo: supposta che la proprietà in (1) è vera per n (questa è l'ipotesi induttiva), verichiamo per n+1 ! n+1 X n X (2k − 1) = (2k − 1) + (2(n + 1) − 1) = n2 + (2n + 1) = (n + 1)2 k=1 k=1 Pn 2 dove abbiamo sostituito ( k=1 (2k − 1)) con n grazie all'ipotesi induttiva. Visto che la proprietà in (1) vale per n = 1 (caso base) e se vale per n allora vale per n + 1 (passo induttivo), la proprietà vale per qualunque n ≥ 1. Schema dell'induzione completa: Sia P (n) una proprietà che dipende da una variabile intera n ∈ N. Se P (n) vale per n = 0, 1,..., k e per ogni n ≥ k vale (P (0) ∧ P (1) ∧... ∧ P (n)) =⇒ P (n + 1) allora P (n) vale per ogni n ∈ N. Cioè ( P (0) ∧ P (1) ∧... ∧ P (k) ∧ (∀n ≥ k.(P (0) ∧ P (1) ∧... ∧ P (n)) =⇒ P (n + 1)) ) =⇒ ∀n ∈ N.P (n) dove P (0) ∧ P (1) ∧... ∧ P (k) è il caso base e (∀n ≥ k.(P (0) ∧ P (1) ∧... ∧ P (n)) =⇒ P (n + 1)) è il passo induttivo. Inoltre, P (0) ∧ P (1) ∧... ∧ P (k) viene chiamata l'ipotesi induttiva. In parole: una proprietà P (n) che vale per n = 0, 1,..., k (caso base) e se vale per 0, 1,..., n allora vale per n+1 (passo induttivo) vale per ogni n ≥ 0. Dimostriamo il seguente teorema con induzione completa. Teorema: Ogni numero naturale n≥2 è un numero primo oppure è esprimibile come prodotto di numeri primi. 2 Dimostrazione: Procediamo con induzione su n. Caso base. L'asserto è vero per n=2 perché 2 è un numero primo. Passo induttivo. Dobbiamo dimostrare che se l'asserto è vero per ogni n0 ∈ {2, 3,..., n} allora è vero per n + 1: se n + 1 è primo allora l'asserto è banalmente vero; se n + 1 non è primo allora si può esprimere n + 1 come il prodotto di due numeri più piccoli n1 , n2 , cioè n + 1 = n1 · n2 con 1 < n1 < n e 1 < n2 < n; per ipotesi induttiva, sia n1 sia n2 è un numero primo oppure è esprimibile come prodotto di numeri primi; segue che anche n + 1 = n1 · n2 è esprimibile come prodotto di numeri primi. Per il principio dell'induzione completa, l'asserto è vera per ogni n ≥ 2. 3 Dimostrazione di correttezza di algoritmi ricorsivi con induzione Il problema delle torre di Hanoi. Dati tre pioli il piolo sorgente con sopra n dischi di diametro crescente, il piolo d'appoggio senza dischi, e il piolo destinazione senza dischi, il compito è spostare la torre dal piolo sorgente al piolo destinazione, sfruttando il piolo d'appoggio, muovendo un disco alla volta, senza mai sovrapporre un disco più grande ad uno più piccolo. Per esempio, con tre dischi da spostare dal piolo A al piolo C, le mosse sono 23 − 1: Sviluppiamo un algoritmo ricorsivo per risolvere il problema in presenza di n dischi. Caso base. Quando il numero di dischi da spostare è 1, il problema è triviale. Ricorsione. Supponendo che siamo in grado di risolvere il problema correttamente con n−1 dischi, si può risolvere il problema con n dischi in tre passaggi: 1. sposta n−1 dischi dal piolo sorgente al piolo d'appoggio; 2. sposta un disco dal piolo sorgente al piolo destinazione; 3. sposta n−1 dischi dal piolo d'appoggio al piolo destinazione. In pseudo-codice: 1: MoveTower(n, A, B, C ). n dischi da spostare dal piolo A al piolo C utilizzando il piolo B come appoggio; Precondizione: A non è vuota e la base di A ha un diametro più piccolo del disco più in alto sia di B che di C; Postcondizione: n dischi sono spostati dal piolo A al piolo C; 2: if n = 1 then 3: move 1 disk from A to C 3  4: else 5: MoveTower(n − 1, A, C, B ) 6: move 1 disk from A to C 7: MoveTower(n − 1, B, A, C ) 8: end if Simulazione dell'algoritmo con 3 dischi da spostare dal piolo 1 al piolo 3 utilizzando il piolo 2 come appoggio. Dopo ogni spostamento viene indicato lo stato del sistema. call_hanoi(n:3,source:1,spare:2,dest:3) call_hanoi(n:2,source:1,spare:3,dest:2) call_hanoi(n:1,source:1,spare:2,dest:3) move 1 -> 3: 2,0,1 end_hanoi(n:1,source:1,spare:2,dest:3) move 1 -> 2: 1,1,1 call_hanoi(n:1,source:3,spare:1,dest:2) move 3 -> 2: 1,2,0 end_hanoi(n:1,source:3,spare:1,dest:2) end_hanoi(n:2,source:1,spare:3,dest:2) move 1 -> 3: 0,2,1 call_hanoi(n:2,source:2,spare:1,dest:3) call_hanoi(n:1,source:2,spare:3,dest:1) move 2 -> 1: 1,1,1 end_hanoi(n:1,source:2,spare:3,dest:1) move 2 -> 3: 1,0,2 call_hanoi(n:1,source:1,spare:2,dest:3) move 1 -> 3: 0,0,3 end_hanoi(n:1,source:1,spare:2,dest:3) end_hanoi(n:2,source:2,spare:1,dest:3) end_hanoi(n:3,source:1,spare:2,dest:3) Teorema: L'algoritmo precedente è corretto. Dimostrazione: Procediamo con induzione su n. Caso base. Con n=1 è triviale che l'algoritmo sia corretto. Passo induttivo. Dobbiamo dimostrare che se l'algoritmo è corretto con n − 1 dischi (ipotesi induttiva) allora è corretto con n dischi. Con n dischi: all'inizio i numeri di dischi sui pioli sono: n, 0, 0 MoveTower(n − 1, A, C, B ) sposta, grazie all'ipotesi induttiva, correttamente n−1 dischi dal piolo A al piolo B; dopodiché abbiamo 1, n − 1, 0 dischi sui pioli dopo move 1 disk from A to C  la situazione è 0, n − 1, 1 MoveTower(n − 1, B, A, C ) sposta, grazie all'ipotesi induttiva, correttamente n − 1 dischi dal piolo B al piolo C ; dopodiché abbiamo 0, 0, n dischi sui pioli. Quindi se l'algoritmo è corretto con n − 1 dischi allora è corretto con n dischi. Per il principio di induzione, l'algoritmo è corretto per ogni n ≥ 1. Il problema della divisione intera. Precondizioni: a ≥ 0, b > 0 numeri interi; Postcondizioni: i risultati sono due interi q, r tali che a = b·q+r con 0≤r 0, procediamo con induzione completa su a. Casi base. Se a < b, cioè per ogni a ∈ {0, 1,..., b − 1} l'algoritmo restituisce q = 0, r = a che è chiaramente corretto. Passo induttivo. Dobbiamo dimostrare che, in caso di a ≥ b, se l'algoritmo è corretto per ogni a0 < a allora l'algoritmo è corretto per a: se con a0 = a − b, b l'algoritmo restituisce q 0 , r0 allora con a, b restituisce q = q 0 + 1, r = r0 0 secondo l'ipotesi induttiva la risposta con a , b è corretta e quindi a0 = a − b = b · q 0 + r0 ∧ 0 ≤ r0 < b da dove segue che a = b · q 0 + b + r0 = b(q 0 + 1) + r0 ∧ 0 ≤ r0 < b e visto che q = q 0 + 1, r = r0 abbiamo a=b·q+r∧0≤r