Esercizi · Correttezza¶
Esercizi · Capitolo 13 · ogni soluzione si apre con un clic · Capitolo 13: Correttezza · Eserciziario, volume 4 (PDF)
Negli esercizi di questo capitolo la correttezza di un ciclo si dimostra con un invariante di ciclo, come nel capitolo «Correttezza», seguendo lo schema seguente.
Un invariante di ciclo è una proprietà delle variabili che è vera ogni volta che viene valutata la condizione del ciclo. Per dimostrare la correttezza del ciclo:
-
Inizializzazione: l'invariante è vero prima della prima iterazione;
-
Conservazione: se l'invariante è vero prima di un'iterazione, è vero prima della successiva;
-
Terminazione: il ciclo termina dopo un numero finito di iterazioni (un numero naturale diminuisce strettamente a ogni iterazione), e l'invariante, insieme alla negazione della condizione del ciclo, fornisce l'output corretto.
Un sotto-array \(a[l..r]\) con \(l>r\) è vuoto, e una somma vuota è uguale a \(0\). Per mostrare che un algoritmo è sbagliato basta un controesempio.
Esercizio 13.1: Correttezza (E1)
Consideriamo il seguente algoritmo, che calcola il valore minimo di un array \(a[1..n]\) di \(n\ge 1\) numeri naturali.
Domande
-
Enunciare un invariante di ciclo per il ciclo while di
FindMinimum. -
Verificare l'invariante di ciclo sull'array \(a=[7,3,9,2,5,2]\), mostrando i valori di \(i\) e \(min\) ogni volta che viene valutata la condizione alla riga 4.
-
Dimostrare la correttezza di
FindMinimum(inizializzazione, conservazione, terminazione). -
Uno studente sostituisce la riga 2 con \(min := 0\). Mostrare, con un controesempio, che il nuovo algoritmo è sbagliato, e indicare quale proprietà dell'invariante di ciclo non vale.
Soluzione
-
Invariante di ciclo:
Ogni volta che viene valutata la condizione alla riga 4,
\[ min=\min\{a[1],a[2],\dots,a[i-1]\}. \] -
For \(a=[7,3,9,2,5,2]\) (\(n=6\)):
\(i\) \(min\) \(a[1..i-1]\) \(\min\{a[1],\dots,a[i-1]\}\) 2 7 \([7]\) 7 3 3 \([7,3]\) 3 4 3 \([7,3,9]\) 3 5 2 \([7,3,9,2]\) 2 6 2 \([7,3,9,2,5]\) 2 7 2 \([7,3,9,2,5,2]\) 2 (il ciclo termina) L'invariante vale a ogni valutazione, e l'algoritmo restituisce \(2\).
-
Dimostrazione di correttezza.
-
Inizializzazione. Prima della prima iterazione \(min=a[1]\) e \(i=2\). Il sotto-array \(a[1..1]\) ha il solo elemento \(a[1]\), il cui minimo è \(a[1]=min\).
-
Conservazione. Supponiamo \(min=\min\{a[1],\dots,a[i-1]\}\) e \(i\le n\). Se \(a[i]<min\), la riga 6 pone \(min\leftarrow a[i]\), che è minore di tutti gli elementi di \(a[1..i-1]\); altrimenti \(min\le a[i]\) e \(min\) non cambia. In entrambi i casi \(min=\min\{a[1],\dots,a[i]\}\). La riga 8 pone \(i\leftarrow i+1\), quindi l'invariante vale con il nuovo valore di \(i\).
-
Terminazione. La variabile \(i\) parte da \(2\le n+1\) e aumenta di \(1\) a ogni iterazione, quindi il ciclo termina dopo \(n-1\) iterazioni, quando \(i=n+1\). Sostituendo \(i=n+1\) nell'invariante:
\[ min=\min\{a[1],\dots,a[n]\}, \]che è restituito alla riga 10. Quindi l'algoritmo è corretto.
-
-
Con \(min:=0\), consideriamo \(a=[3,5]\). Poiché nessun elemento è minore di \(0\), la riga 6 non viene mai eseguita e l'algoritmo restituisce \(0\), mentre l'output corretto è \(3\). Quindi l'algoritmo è sbagliato.
La proprietà che non vale è l'inizializzazione: prima della prima iterazione \(i=2\) e \(min=0\), mentre \(\min\{a[1]\}=a[1]=3\neq 0\). La conservazione è ancora vera (se l'invariante valesse, continuerebbe a valere), ma poiché è falso all'inizio, l'argomento di terminazione non può essere applicato. In effetti, poiché le componenti sono numeri naturali, l'algoritmo restituisce sempre \(\min\{0,a[2],\dots,a[n]\}=0\), che è corretto solo se almeno una componente dell'array è uguale a \(0\).
Esercizio 13.2: Correttezza (E2)
Consideriamo il seguente algoritmo.
Domande
-
Che cosa calcola l'algoritmo? Enunciare un invariante di ciclo per il suo ciclo while.
-
Verificare l'invariante di ciclo sull'array \(a=[4,1,7,3]\), mostrando i valori di \(i\) e \(s\) ogni volta che viene valutata la condizione alla riga 4.
-
Dimostrare la correttezza di
ArraySum. -
Uno studente modifica la riga 3 in \(i:=0\) e la riga 4 in “while \(i<n\)”, mantenendo \(a[i]\) alla riga 5. Il nuovo algoritmo è corretto?
Soluzione
-
L'algoritmo calcola la somma degli elementi dell'array:
\[ s=\sum_{k=1}^{n}a[k]. \]Invariante di ciclo:
Ogni volta che viene valutata la condizione alla riga 4,
\[ s=\sum_{k=1}^{i-1}a[k], \]dove una somma vuota (\(i=1\)) è uguale a \(0\).
-
For \(a=[4,1,7,3]\) (\(n=4\)):
\(i\) \(s\) \(\sum_{k=1}^{i-1}a[k]\) 1 0 \(0\) (somma vuota) 2 4 \(4\) 3 5 \(4+1=5\) 4 12 \(4+1+7=12\) 5 15 \(4+1+7+3=15\) (il ciclo termina) L'algoritmo restituisce \(15\).
-
Dimostrazione di correttezza.
-
Inizializzazione. Prima della prima iterazione \(s=0\) e \(i=1\); la somma \(\sum_{k=1}^{0}a[k]\) è vuota, quindi uguale a \(0=s\).
-
Conservazione. Supponiamo \(s=\sum_{k=1}^{i-1}a[k]\) e \(i\le n\). La riga 5 dà
\[ s+a[i]=\sum_{k=1}^{i-1}a[k]+a[i]=\sum_{k=1}^{i}a[k], \]e la riga 6 incrementa \(i\) di \(1\), quindi l'invariante vale con il nuovo valore di \(i\).
-
Terminazione. La variabile \(i\) parte da \(1\) e aumenta di \(1\) a ogni iterazione, quindi il ciclo termina dopo \(n\) iterazioni, quando \(i=n+1\). Sostituendo \(i=n+1\) nell'invariante si ottiene \(s=\sum_{k=1}^{n}a[k]\), che è restituito alla riga 8. Quindi l'algoritmo è corretto.
-
-
No. Con \(i:=0\) la prima iterazione accede ad \(a[0]\), che non esiste in un array \(a[1..n]\); inoltre, la condizione \(i<n\) ferma il ciclo quando \(i=n\), quindi \(a[n]\) non viene mai sommato. In termini di invariante, l'invariante naturale del nuovo ciclo è \(s=\sum_{k=0}^{i-1}a[k]\), e alla terminazione (\(i=n\)) dà \(s=\sum_{k=0}^{n-1}a[k]\neq\sum_{k=1}^{n}a[k]\): il passo di terminazione non fornisce la proprietà richiesta. Per esempio, su \(a=[4,1,7,3]\) l'elemento \(a[4]=3\) non viene mai sommato, quindi anche ignorando l'accesso non valido il risultato non può essere \(15\). Questo è un errore tipico che si ottiene mescolando codice con indici da \(0\) (come in C++) e pseudocodice con indici da \(1\).
Esercizio 13.3: Correttezza (E3)
Consideriamo l'algoritmo SelectionSort, che ordina in modo non decrescente un array \(a[1..n]\) di \(n\ge 1\) numeri naturali.
Domande
Soluzione
-
Consideriamo un'iterazione del ciclo esterno con un dato valore di \(i\). Il ciclo interno non modifica l'array. Il suo invariante è:
Ogni volta che viene valutata la condizione alla riga 6, \(i\le \mathit{minIdx}\le j-1\) e
\[ a[\mathit{minIdx}]=\min\{a[i],a[i+1],\dots,a[j-1]\}. \]-
Inizializzazione. Le righe 4–5 pongono \(\mathit{minIdx}=i\) e \(j=i+1\): il sotto-array \(a[i..j-1]=a[i..i]\) ha il solo elemento \(a[i]=a[\mathit{minIdx}]\).
-
Conservazione. Supponiamo l'invariante e \(j\le n\). Se \(a[j]<a[\mathit{minIdx}]\), allora \(a[j]\) è minore di tutti gli elementi di \(a[i..j-1]\) e la riga 8 pone \(\mathit{minIdx}\leftarrow j\); altrimenti \(a[\mathit{minIdx}]\le a[j]\). In entrambi i casi \(a[\mathit{minIdx}]=\min\{a[i],\dots,a[j]\}\) e \(i\le\mathit{minIdx}\le j\). La riga 10 pone \(j\leftarrow j+1\), quindi l'invariante vale con il nuovo \(j\).
-
Terminazione. \(j\) aumenta di \(1\) a partire da \(i+1\le n\), quindi il ciclo si ferma quando \(j=n+1\). Allora \(a[\mathit{minIdx}]=\min\{a[i],\dots,a[n]\}\): \(\mathit{minIdx}\) è l'indice di un elemento minimo di \(a[i..n]\).
-
-
Invariante del ciclo esterno:
Ogni volta che viene valutata la condizione alla riga 3:
-
(P1) l'array \(a[1..n]\) contiene gli elementi originali (è un riordinamento dell'input);
-
(P2) il sotto-array \(a[1..i-1]\) è ordinato in modo non decrescente;
-
(P3) ogni elemento di \(a[1..i-1]\) è \(\le\) ogni elemento di \(a[i..n]\).
-
-
Per \(a=[29,10,14,37,13]\) (\(n=5\)); il prefisso ordinato \(a[1..i-1]\) è evidenziato in blu:
\(i\) \(a[1]\) \(a[2]\) \(a[3]\) \(a[4]\) \(a[5]\) minimo di \(a[i..n]\) 1 29 10 14 37 13 \(a[2]=10\): scambio di \(a[1],a[2]\) 2 10 29 14 37 13 \(a[5]=13\): scambio di \(a[2],a[5]\) 3 10 13 14 37 29 \(a[3]=14\): nessuno scambio 4 10 13 14 37 29 \(a[5]=29\): scambio di \(a[4],a[5]\) 5 10 13 14 29 37 il ciclo termina (\(i=n\)) A ogni riga il prefisso blu è ordinato, e ogni elemento blu è \(\le\) ogni elemento non blu: per esempio, per \(i=4\), \(\max\{10,13,14\}=14\le\min\{37,29\}=29\).
-
Dimostrazione di correttezza.
-
Inizializzazione. Prima della prima iterazione \(i=1\) e nulla è stato modificato: (P1) vale, e \(a[1..0]\) è vuoto, quindi (P2) e (P3) valgono banalmente.
-
Conservazione. Supponiamo (P1)–(P3) e \(i\le n-1\). Per il punto 1, dopo il ciclo interno
\[ a[\mathit{minIdx}]=\min\{a[i],\dots,a[n]\}. \]Le righe 12–15 scambiano \(a[i]\) e \(a[\mathit{minIdx}]\) (se sono posizioni diverse). Uno scambio si limita a scambiare due elementi, quindi (P1) vale ancora. Ora \(a[i]\) è il minimo di \(a[i..n]\), quindi:
-
per (P3), \(a[i]\ge\) ogni elemento di \(a[1..i-1]\), e poiché \(a[1..i-1]\) è ordinato (P2), \(a[1..i]\) è ordinato;
-
\(a[i]\le\) ogni elemento di \(a[i+1..n]\), perché \(a[i]\) è il minimo di \(a[i..n]\) e lo scambio riordina solo i valori nelle posizioni \(i..n\); per lo stesso motivo, per (P3) ogni elemento di \(a[1..i-1]\) è \(\le\) ogni elemento di \(a[i+1..n]\). Quindi ogni elemento di \(a[1..i]\) è \(\le\) ogni elemento di \(a[i+1..n]\).
La riga 17 pone \(i\leftarrow i+1\), quindi (P1)–(P3) valgono con il nuovo valore di \(i\).
-
-
Terminazione. Il ciclo interno termina sempre (punto 1), e \(i\) aumenta di \(1\) a partire da \(1\); il ciclo esterno si ferma quando \(i=n\) per la prima volta (dopo \(n-1\) iterazioni; se \(n=1\) non viene mai eseguito e \(i=1=n\)). Sostituendo \(i=n\): \(a[1..n-1]\) è ordinato (P2) e ogni elemento di \(a[1..n-1]\) è \(\le a[n]\) (P3); quindi l'intero array \(a[1..n]\) è ordinato e, per (P1), contiene gli elementi originali. Quindi l'algoritmo è corretto.
Notiamo che il ciclo esterno richiede solo \(n-1\) iterazioni: quando le prime \(n-1\) posizioni sono corrette, l'ultimo elemento è automaticamente nella sua posizione corretta.
-
Esercizio 13.4: Correttezza (E4)
Consideriamo l'algoritmo LinearSearch, che determina se un valore \(m\) è uno degli elementi di un array \(a[1..n]\) di \(n\) numeri naturali (non necessariamente ordinato).
Domande
-
Enunciare un invariante di ciclo per il ciclo while di
LinearSearch. -
Verificare l'invariante di ciclo sull'array \(a=[8,3,6,3,9]\) per \(m=6\) e per \(m=5\).
-
Dimostrare che
LinearSearchè corretto. Dimostrare anche che, quando \(m\) è nell'array, l'indice restituito è il più piccolo indice \(k\) tale che \(a[k]=m\). -
Uno studente scambia le righe 4–5 e la riga 7, cioè il corpo del ciclo prima incrementa \(i\) e poi controlla se \(a[i]=m\). Trovare un controesempio che mostri che il nuovo algoritmo è sbagliato, e indicare quale proprietà dell'invariante di ciclo non vale.
Soluzione
-
Invariante di ciclo:
Ogni volta che viene valutata la condizione alla riga 3, \(1\le i\le n+1\) e \(m\) non è nel sotto-array \(a[1..i-1]\):
\[ a[k]\neq m\qquad \text{per ogni } k\in\{1, 2, \dots, i-1\}. \] -
Per \(a=[8,3,6,3,9]\):
\(m\) \(i\) \(a[1..i-1]\) azione 6 1 \([\ ]\) \(a[1]=8\neq 6\) 2 \([8]\) \(a[2]=3\neq 6\) 3 \([8,3]\) \(a[3]=6=m\) \(\Rightarrow\) restituisce \(3\) 5 1 \([\ ]\) \(a[1]=8\neq 5\) 2 \([8]\) \(a[2]=3\neq 5\) 3 \([8,3]\) \(a[3]=6\neq 5\) 4 \([8,3,6]\) \(a[4]=3\neq 5\) 5 \([8,3,6,3]\) \(a[5]=9\neq 5\) 6 \([8,3,6,3,9]\) \(i>n\) \(\Rightarrow\) restituisce \(-1\) A ogni valutazione, \(m\) non compare in \(a[1..i-1]\).
-
Dimostrazione di correttezza.
-
Inizializzazione. Prima della prima iterazione \(i=1\) e \(a[1..0]\) è vuoto, quindi non contiene \(m\).
-
Conservazione. Supponiamo l'invariante e \(i\le n\). Se \(a[i]=m\), l'algoritmo restituisce \(i\) (riga 5), che è un output corretto. Altrimenti \(a[i]\neq m\), quindi \(m\) non è in \(a[1..i]\); la riga 7 pone \(i\leftarrow i+1\) e l'invariante vale con il nuovo valore di \(i\).
-
Terminazione. \(i\) aumenta di \(1\) a partire da \(1\), quindi il ciclo esegue al più \(n\) iterazioni. L'algoritmo finisce in uno di due modi:
-
restituisce \(i\) con \(a[i]=m\): corretto. Inoltre, per l'invariante \(a[k]\neq m\) per ogni \(k<i\), quindi \(i\) è il più piccolo indice con \(a[i]=m\);
-
la condizione alla riga 3 è falsa, cioè \(i=n+1\): per l'invariante \(m\) non è in \(a[1..n]\), e l'algoritmo restituisce correttamente \(-1\).
Quindi l'algoritmo è corretto.
-
-
-
Il nuovo corpo è: \(i\leftarrow i+1\); if \(a[i]=m\) then return \(i\). Consideriamo \(a=[6,3]\) e \(m=6\). Nella prima iterazione \(i\) diventa \(2\) e \(a[2]=3\neq 6\); nella seconda iterazione \(i\) diventa \(3\) e l'algoritmo accede ad \(a[3]\), che è fuori dall'array; in ogni caso \(a[1]=6\) non viene mai controllato, quindi l'algoritmo non può restituire \(1\).
La proprietà che non vale è la conservazione: se \(m\) non è in \(a[1..i-1]\) all'inizio dell'iterazione, dopo il corpo sappiamo solo che \(m\) non è in \(a[1..i-1]\) e che \(a[i+1]\neq m\), ma non sappiamo nulla su \(a[i]\). Con il nuovo valore \(i+1\), l'invariante richiederebbe che \(m\) non sia in \(a[1..i]\), cosa che non è garantita: nell'esempio, prima della seconda valutazione della condizione \(i=2\) e \(a[1]=6=m\).
Esercizio 13.5: Correttezza (E5)
Consideriamo i due algoritmi seguenti, che dovrebbero calcolare \(x^n\) per due numeri naturali \(x\ge 1\) e \(n\ge 0\) (ricordiamo che \(x^0=1\)).
Domande
-
Enunciare un invariante di ciclo per il ciclo while di
Powere verificarlo per \(x=3\), \(n=4\). -
Dimostrare la correttezza di
Power, incluso il caso \(n=0\). -
Mostrare che lo stesso invariante non è un invariante di ciclo di
WrongPower: quale delle tre proprietà non vale? Dare un controesempio che mostri cheWrongPowerè sbagliato, con una traccia per \(x=2\), \(n=3\). -
Trovare l'invariante di ciclo corretto di
WrongPowere usarlo per determinare esattamente che cosa calcolaWrongPower. Per quali input il suo output è corretto?
Soluzione
-
Invariante di ciclo di
Power:Ogni volta che viene valutata la condizione alla riga 4, \(1\le i\le n+1\) e
\[ p=x^{\,i-1}. \]Per \(x=3\), \(n=4\):
\(i\) \(p\) \(x^{i-1}\) 1 1 \(3^0=1\) 2 3 \(3^1=3\) 3 9 \(3^2=9\) 4 27 \(3^3=27\) 5 81 \(3^4=81\) (il ciclo termina) L'algoritmo restituisce \(81=3^4\).
-
Dimostrazione di correttezza di
Power.-
Inizializzazione. Prima della prima iterazione \(p=1\) e \(i=1\), quindi \(p=x^0=x^{i-1}\); inoltre \(1\le i\le n+1\) poiché \(n\ge 0\).
-
Conservazione. Supponiamo \(p=x^{i-1}\) e \(i\le n\). La riga 5 dà \(p\cdot x=x^{i-1}\cdot x=x^{i}\), e la riga 6 pone \(i\leftarrow i+1\le n+1\). Con il nuovo valore di \(i\), \(p=x^{i-1}\).
-
Terminazione. \(i\) aumenta di \(1\) a partire da \(1\le n+1\), quindi il ciclo termina dopo esattamente \(n\) iterazioni, quando \(i=n+1\). Sostituendo \(i=n+1\): \(p=x^{n}\), che è restituito alla riga 8.
Se \(n=0\), la condizione \(1\le 0\) è falsa alla prima valutazione, il ciclo non viene mai eseguito e l'algoritmo restituisce \(p=1=x^0\), in accordo con la dimostrazione (inizializzazione e terminazione coincidono, con \(i=1=n+1\)).
-
-
Per
WrongPower, l'inizializzazione non vale: prima della prima iterazione \(i=1\) e \(p=x\), mentre \(x^{i-1}=x^0=1\). Quindi \(p\neq x^{i-1}\) ogni volta che \(x\ge 2\). (La conservazione è ancora vera: se valesse \(p=x^{i-1}\), il corpo la preserverebbe; ma l'“induzione” non ha un caso base valido.)Controesempio: \(x=2\), \(n=3\), per cui \(x^n=8\).
\(i\) \(p\) \(x^{i-1}\) \(x^{i}\) 1 2 1 2 2 4 2 4 3 8 4 8 4 16 8 16 (il ciclo termina) WrongPowerrestituisce \(16\neq 8=2^3\), quindi è sbagliato. -
La tabella suggerisce l'invariante \(p=x^{\,i}\), che è un invariante di ciclo corretto di
WrongPower:-
Inizializzazione: \(p=x=x^1=x^i\) con \(i=1\);
-
Conservazione: se \(p=x^i\) e \(i\le n\), dopo il corpo \(p=x^{i+1}\) e \(i\) è incrementato di \(1\);
-
Terminazione: il ciclo termina con \(i=n+1\), quindi \(p=x^{n+1}\).
Quindi
WrongPowercalcola \(x^{n+1}\). Il suo output è corretto, cioè \(x^{n+1}=x^n\), se e solo se \(x^n(x-1)=0\), ovvero (poiché \(x\ge 1\)) se e solo se \(x=1\). Per ogni \(x\ge 2\) e ogni \(n\ge 0\) è sbagliato: basta un controesempio per mostrare che un algoritmo non è corretto. -