Correttezza

Parte 4 · Analisi degli algoritmi · Capitolo 13 · Dispensa, volume 4 (PDF) · Esercizi: Correttezza · App: L'invariante di ciclo

13.1 Correttezza di un algoritmo

• I capitoli precedenti hanno misurato quanto costa un algoritmo: la dimensione del suo input e il suo tempo di esecuzione. Prima di chiedersi quanto sia veloce un algoritmo, però, dobbiamo essere sicuri che faccia ciò che promette. Questo capitolo presenta lo strumento standard per dimostrarlo, l'invariante di ciclo, e lo applica ad algoritmi già incontrati nei capitoli «Ordinamento», «Ricerca lineare e ricerca binaria» e «Algoritmi numerici»: Find Maximum, Insertion Sort, Binary Search e l'algoritmo di Euclide.

• La prima parte dell'analisi di un algoritmo consiste nel determinarne la correttezza, cioè nel dimostrare che calcola l'output corretto per ogni possibile istanza di input.

• Provare un algoritmo su alcune istanze può mostrare che è sbagliato (basta un controesempio), ma non può mai mostrare che è corretto: le istanze di input sono infinite. La correttezza va dimostrata.

Definizione 13.1: algoritmo corretto

Un algoritmo è corretto se, per ogni istanza di input \(I\) del problema, termina dopo un numero finito di passi e restituisce l'output corretto per \(I\).

• Gli algoritmi che consideriamo sono costituiti da sequenze di istruzioni e da cicli. Le sequenze di istruzioni sono facili da analizzare, mentre un ciclo esegue le stesse istruzioni un numero di volte che dipende dall'input.

La correttezza di un algoritmo si basa sulla correttezza dei suoi cicli. La correttezza di un ciclo si dimostra per mezzo di un invariante di ciclo.

13.1.1 Invarianti di ciclo

Definizione 13.2: invariante di ciclo

Un invariante di ciclo è una proprietà delle variabili di un algoritmo che è vera ogni volta che viene valutata la condizione di un ciclo, cioè prima della prima iterazione del ciclo e dopo ogni iterazione del ciclo.

• Per dimostrare la correttezza di un algoritmo per mezzo di un invariante di ciclo dobbiamo mostrare tre cose:

  1. Inizializzazione: l'invariante di ciclo è vero prima della prima iterazione del ciclo.

  2. Conservazione: se l'invariante di ciclo è vero prima di un'iterazione del ciclo, allora rimane vero alla fine dell'iterazione, o equivalentemente, è vero prima dell'iterazione successiva.

  3. Terminazione: il ciclo termina dopo un numero finito di iterazioni. Quando il ciclo termina, l'invariante di ciclo, insieme al fatto che la condizione del ciclo è falsa, fornisce una proprietà utile che mostra che l'algoritmo è corretto.

• Notiamo la somiglianza con l'induzione matematica, dove per dimostrare che una proprietà vale è necessario dimostrare un caso base e un passo induttivo:

  • mostrare che l'invariante vale prima della prima iterazione corrisponde al caso base;

  • mostrare che l'invariante vale da un'iterazione alla successiva corrisponde al passo induttivo.

  La proprietà di terminazione differisce dal consueto uso dell'induzione matematica, in cui il passo induttivo viene applicato infinite volte: qui l'“induzione” si ferma quando il ciclo termina.

• Per dimostrare che un ciclo termina, di solito si individua un numero naturale (per esempio \(n-i+1\) o la lunghezza di un sotto-array) che diminuisce strettamente a ogni iterazione e che deve essere positivo perché il ciclo continui. Poiché un numero naturale non può diminuire all'infinito, il ciclo termina.

Schema di una dimostrazione di correttezza con un invariante di ciclo

1. Enunciare l'invariante: una proprietà delle variabili, vera ogni volta che viene valutata la condizione del ciclo.

2. Inizializzazione: verificarlo con i valori assegnati prima del ciclo.

3. Conservazione: assumerlo insieme alla condizione del ciclo, eseguire il corpo una volta, e verificarlo con i nuovi valori.

4. Terminazione: trovare un numero naturale che diminuisce strettamente a ogni iterazione; poi combinare l'invariante con la negazione della condizione del ciclo per ottenere l'output corretto.

13.2 Correttezza di Find Maximum

Dato un array \(a[1..n]\) di \(n\) numeri interi, con \(n \ge 1\), consideriamo il problema di determinare il valore massimo dell'array.

• Il primo esempio è il ciclo più semplice: una singola scansione dell'array. Questo è lo pseudocodice dell'algoritmo FindMaximum.

Algoritmo: FindMaximum

Input: Un array \(a[1..n]\) di \(n\) numeri interi

Output: Il valore massimo dell'array \(a\)

1function FindMaximum(a, n)

2\(max := a[1]\)

3\(i := 2\)

4while \(i \leq n\) do

5if \(a[i] > max\) then

6\(max \leftarrow a[i]\)

7end

8\(i \leftarrow i + 1\)

9end

10return \(max\)

11end

Esegui in Colab:PythonC++Java

• L'invariante di ciclo del ciclo while di FindMaximum è:

Ogni volta che viene valutata la condizione alla riga 4, la variabile \(max\) è uguale al valore massimo del sotto-array \(a[1..i-1]\):

\[ max=\max\{a[1],a[2],\dots,a[i-1]\}. \]

Esempio 13.1: Invariante di ciclo di FindMaximum

Consideriamo l'array \(a=[9, 12, 3, 16, 19, 11, 12]\) con \(n=7\). La tabella mostra i valori di \(i\) e \(max\) ogni volta che viene valutata la condizione alla riga 4:

\(i\)	\(max\)	\(a[1..i-1]\)	\(\max\{a[1],\dots,a[i-1]\}\)
2	9	\([9]\)	9
3	12	\([9,12]\)	12
4	12	\([9,12,3]\)	12
5	16	\([9,12,3,16]\)	16
6	19	\([9,12,3,16,19]\)	19
7	19	\([9,12,3,16,19,11]\)	19
8	19	\([9,12,3,16,19,11,12]\)	19 (il ciclo termina)

A ogni valutazione l'invariante vale. Quando il ciclo termina \(i=n+1=8\), e l'algoritmo restituisce \(19\), il massimo dell'intero array.

• Usando l'invariante di ciclo possiamo dimostrare la correttezza dell'algoritmo FindMaximum, enunciata dalla seguente osservazione.

Osservazione 13.3

Dato un array \(a[1..n]\) di \(n \ge 1\) numeri interi, l'algoritmo FindMaximum termina e restituisce

\[ \max\{a[1],a[2],\dots,a[n]\}. \]

Dimostrazione

Dimostriamo le tre proprietà dell'invariante di ciclo.

• Inizializzazione. Prima della prima iterazione, le righe 2 e 3 pongono \(max=a[1]\) e \(i=2\). Il sotto-array \(a[1..i-1]=a[1..1]\) è costituito dal solo elemento \(a[1]\), il cui massimo è \(a[1]=max\). Quindi l'invariante vale.

• Conservazione. Supponiamo che, prima di un'iterazione, \(max=\max\{a[1],\dots,a[i-1]\}\). Il corpo del ciclo confronta \(a[i]\) con \(max\) (riga 5):

  • se \(a[i]>max\), allora la riga 6 pone \(max \leftarrow a[i]\), e \(a[i]\) è maggiore di tutti gli elementi di \(a[1..i-1]\);

  • se \(a[i]\le max\), allora \(max\) non cambia ed è maggiore o uguale a \(a[i]\).

  In entrambi i casi, alla fine del corpo

  \[ max=\max\{a[1],\dots,a[i-1],a[i]\}. \]

  La riga 8 incrementa \(i\) di \(1\), quindi, con il nuovo valore di \(i\), si ha di nuovo \(max=\max\{a[1],\dots,a[i-1]\}\). Quindi l'invariante vale prima dell'iterazione successiva.

• Terminazione. La variabile \(i\) parte da \(2\le n+1\) e aumenta di \(1\) a ogni iterazione, quindi il ciclo termina dopo esattamente \(n-1\) iterazioni, quando per la prima volta \(i=n+1\). Sostituendo \(i=n+1\) nell'invariante di ciclo otteniamo

  \[ max=\max\{a[1],a[2],\dots,a[n]\}, \]

  che è il valore restituito alla riga 10. Quindi l'algoritmo è corretto.

□

13.3 Correttezza di Insertion Sort

Dato un array \(a[1..n]\) di \(n\) numeri naturali, con \(n\ge 1\), consideriamo il problema di riordinare gli elementi dell'array in modo non decrescente:

\[ a[1] \le a[2] \le \cdots \le a[n]. \]

• Con due cicli annidati la dimostrazione richiede due invarianti, uno per ciascun ciclo. Questo è lo pseudocodice dell'algoritmo InsertionSort.

Algoritmo: InsertionSort

Input: Un array \(a[1..n]\) di \(n\) numeri naturali

Output: L'array \(a\) ordinato in modo non decrescente

1function InsertionSort(a, n)

2\(i := 2\)

3while \(i \le n\) do

4\(key := a[i]\)// Elemento da inserire

5\(j := i - 1\)

6while \(j \ge 1\) and \(a[j] > key\) do

7\(a[j+1]\) \(\leftarrow\) \(a[j]\)// Sposta l'elemento a destra

8\(j\) \(\leftarrow\) \(j - 1\)

9end

10\(a[j+1]\) \(\leftarrow\) \(key\)// Inserisce key nella posizione corretta

11\(i \leftarrow i + 1\)

12end

13end

Esegui in Colab:PythonC++Java

• La condizione alla riga 6 è valutata da sinistra a destra, e la seconda parte è valutata solo se la prima è vera: quando \(j=0\) la condizione è falsa e l'elemento inesistente \(a[0]\) non viene mai acceduto.

• L'algoritmo contiene due cicli annidati. Dimostriamo prima che cosa fa una singola esecuzione del ciclo while interno (righe 6–8), e poi usiamo questo risultato per dimostrare la correttezza del ciclo while esterno (righe 3–11).

13.3.1 Il ciclo interno

• Consideriamo un'iterazione del ciclo esterno, con un dato valore di \(i \in \{2,3,\dots,n\}\). Indichiamo con

  \[ b[1..i] \]

  il contenuto del sotto-array \(a[1..i]\) all'inizio di questa iterazione (cioè quando la condizione alla riga 3 è vera), e supponiamo che \(b[1..i-1]\) sia ordinato in modo non decrescente. Dopo la riga 4 si ha \(key=b[i]\).

• L'invariante di ciclo del ciclo while interno è:

Ogni volta che viene valutata la condizione alla riga 6:

• (I1) \(a[1..j]=b[1..j]\) (i primi \(j\) elementi non sono stati spostati);

• (I2) \(a[j+2..i]=b[j+1..i-1]\) (gli elementi \(b[j+1],\dots,b[i-1]\) sono stati spostati di una posizione a destra);

• (I3) ogni elemento di \(a[j+2..i]\) è strettamente maggiore di \(key\).

Le componenti \(a[i+1..n]\) non vengono mai modificate dal ciclo interno.

• La posizione \(j+1\) è il “buco” in cui verrà inserito \(key\): il suo contenuto attuale è una copia che verrà sovrascritta. Un sotto-array \(a[l..r]\) con \(l>r\) è vuoto, e qualunque proprietà di tutti i suoi elementi è banalmente vera.

Esempio 13.2: Invariante di ciclo del ciclo interno

Consideriamo l'array \(a=[5,2,4,1,3]\) all'inizio dell'iterazione \(i=5\) del ciclo esterno: \(b[1..5]=[1,2,4,5,3]\) e \(key=3\). La tabella mostra l'array ogni volta che viene valutata la condizione alla riga 6.

\(j\)	\(a[1]\)	\(a[2]\)	\(a[3]\)	\(a[4]\)	\(a[5]\)	\(a[1..j]\)	\(a[j+2..5]\)	condizione
4	1	2	4	5	3	\([1,2,4,5]\)	\([\ ]\)	\(a[4]=5>3\): vera
3	1	2	4	5	5	\([1,2,4]\)	\([5]\)	\(a[3]=4>3\): vera
2	1	2	4	4	5	\([1,2]\)	\([4,5]\)	\(a[2]=2\le 3\): falsa

A ogni valutazione \(a[1..j]=b[1..j]\), \(a[j+2..5]=b[j+1..4]\) e tutti gli elementi di \(a[j+2..5]\) sono maggiori di \(3\). Quando il ciclo termina \(j=2\), e la riga 10 pone \(a[3]\leftarrow 3\), ottenendo \(a[1..5]=[1,2,3,4,5]\).

Lemma 13.4: ciclo interno di Insertion Sort

Consideriamo un'iterazione del ciclo esterno di InsertionSort con \(i\in\{2,\dots,n\}\), e sia \(b[1..i]\) il contenuto di \(a[1..i]\) all'inizio dell'iterazione. Se \(b[1..i-1]\) è ordinato in modo non decrescente, allora il ciclo while interno termina e, dopo la riga 10, il sotto-array \(a[1..i]\) contiene gli elementi \(b[1],\dots,b[i]\) ordinati in modo non decrescente, mentre \(a[i+1..n]\) è invariato.

Dimostrazione

Dimostriamo le tre proprietà dell'invariante di ciclo (I1)–(I3).

• Inizializzazione. Prima della prima valutazione della condizione, \(j=i-1\) e nulla è stato modificato. Quindi \(a[1..i-1]=b[1..i-1]\), cioè (I1) vale. I sotto-array \(a[j+2..i]=a[i+1..i]\) e \(b[j+1..i-1]=b[i..i-1]\) sono entrambi vuoti, quindi (I2) e (I3) valgono banalmente.

• Conservazione. Supponiamo che (I1)–(I3) valgano e che la condizione alla riga 6 sia vera, cioè \(j\ge 1\) e \(a[j]>key\). Per (I1), \(a[j]=b[j]\), quindi \(b[j]>key\). La riga 7 pone \(a[j+1]\leftarrow a[j]=b[j]\); quindi, per (I2),

  \[ a[j+1..i]=b[j..i-1], \]

  e tutti questi elementi sono maggiori di \(key\) (per (I3) e \(b[j]>key\)). Le posizioni \(1,\dots,j\) non vengono modificate. La riga 8 pone \(j\leftarrow j-1\). Indicando con \(j'=j-1\) il nuovo valore, si ha \(a[1..j']=b[1..j']\), \(a[j'+2..i]=a[j+1..i]=b[j..i-1]=b[j'+1..i-1]\), e tutti gli elementi di \(a[j'+2..i]\) sono maggiori di \(key\). Quindi (I1)–(I3) valgono prima della valutazione successiva della condizione.

• Terminazione. La variabile \(j\) parte da \(i-1\) e diminuisce di \(1\) a ogni iterazione; poiché il ciclo si ferma al più tardi quando \(j=0\), il ciclo interno esegue al più \(i-1\) iterazioni e termina. Quando termina, si ha \(j=0\) oppure \(a[j]=b[j]\le key\). Per (I1)–(I3):

  • \(a[1..j]=b[1..j]\) è ordinato e, se \(j\ge 1\), il suo elemento più grande \(b[j]\) è \(\le key\);

  • \(a[j+2..i]=b[j+1..i-1]\) è ordinato e tutti i suoi elementi sono \(>key\).

  La riga 10 pone \(a[j+1]\leftarrow key=b[i]\). Quindi

  \[ a[1..i]=\big[\,b[1],\dots,b[j],\ key,\ b[j+1],\dots,b[i-1]\,\big], \]

  che contiene esattamente gli elementi \(b[1],\dots,b[i]\) ed è ordinato in modo non decrescente, perché \(b[1..j]\) è ordinato, \(b[j]\le key< b[j+1]\), e \(b[j+1..i-1]\) è ordinato. Le posizioni \(i+1,\dots,n\) non vengono mai accedute.

□

13.3.2 Il ciclo esterno

• L'invariante di ciclo del ciclo while esterno è:

Ogni volta che viene valutata la condizione alla riga 3, il sotto-array \(a[1..i-1]\) è costituito dagli elementi originariamente in \(a[1..i-1]\), ma ordinati in modo non decrescente, e il sotto-array \(a[i..n]\) è uguale al sotto-array originale \(a[i..n]\).

Esempio 13.3: Invariante di ciclo del ciclo esterno

Consideriamo l'array \(a=[5,2,4,1,3]\) con \(n=5\). La tabella mostra l'array ogni volta che viene valutata la condizione alla riga 3; il sotto-array ordinato \(a[1..i-1]\) è evidenziato in blu.

\(i\)	\(a[1]\)	\(a[2]\)	\(a[3]\)	\(a[4]\)	\(a[5]\)	\(a[1..i-1]\) originale
2	5	2	4	1	3	\([5]\)
3	2	5	4	1	3	\([5,2]\)
4	2	4	5	1	3	\([5,2,4]\)
5	1	2	4	5	3	\([5,2,4,1]\)
6	1	2	3	4	5	\([5,2,4,1,3]\) (il ciclo termina)

• Usando l'invariante di ciclo e il Lemma 13.4 possiamo dimostrare la correttezza dell'algoritmo InsertionSort.

Osservazione 13.5

Dato un array \(a[1..n]\) di \(n\ge 1\) numeri naturali, l'algoritmo InsertionSort termina e, alla fine, l'array \(a[1..n]\) contiene gli elementi originali riordinati in modo non decrescente:

\[ a[1]\le a[2]\le\cdots\le a[n]. \]

Dimostrazione

Dimostriamo le tre proprietà dell'invariante di ciclo del ciclo esterno.

• Inizializzazione. Prima della prima iterazione, \(i=2\) (riga 2) e l'array non è stato modificato. Il sotto-array \(a[1..i-1]=a[1..1]\) è costituito dal singolo elemento originale \(a[1]\), ed è banalmente ordinato. Il sotto-array \(a[2..n]\) è quello originale. Quindi l'invariante vale.

• Conservazione. Supponiamo che l'invariante valga e che \(i\le n\). Allora \(a[1..i-1]\) contiene gli elementi originali di \(a[1..i-1]\) ordinati, e \(a[i]\) è l'elemento originale \(a[i]\). Per il Lemma 13.4, dopo la riga 10 il sotto-array \(a[1..i]\) contiene questi \(i\) elementi, cioè gli elementi originali di \(a[1..i]\), ordinati in modo non decrescente, e \(a[i+1..n]\) è invariato, quindi ancora uguale a quello originale. La riga 11 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, e ogni ciclo interno termina (Lemma 13.4). Quindi il ciclo esterno termina dopo esattamente \(n-1\) iterazioni, quando per la prima volta \(i=n+1\). Sostituendo \(i=n+1\) nell'invariante di ciclo, il sotto-array \(a[1..n]\), cioè l'intero array, è costituito dagli elementi originali ordinati in modo non decrescente. Quindi l'algoritmo è corretto.

□

13.4 Correttezza di Binary Search

Dati un array \(a[1..n]\) di \(n\) numeri naturali ordinato in modo non decrescente e un numero naturale \(m\) da cercare, consideriamo il problema di determinare se \(m\) è uno degli elementi dell'array.

• Nei due algoritmi precedenti il ciclo viene sempre eseguito finché la sua condizione diventa falsa. La ricerca binaria può invece fermarsi in anticipo, con un return dentro il ciclo, e la dimostrazione deve tenere conto di entrambe le uscite. Questo è lo pseudocodice dell'algoritmo BinarySearch (iterativo).

Algoritmo: BinarySearch

Input: Un array \(a[1..n]\) di \(n\) numeri naturali ordinato in modo non decrescente e un valore \(m\) da cercare

Output: Indice di \(m\) in \(a\), oppure \(-1\) se non trovato

1function BinarySearch(a, n, m)

2\(left\) := \(1\)// Estremo sinistro

3\(right\) := \(n\)// Estremo destro

4while \(left \le right\) do

5\(mid\) := \(left + \lfloor (right - left) / 2 \rfloor\)// Indice centrale

6if \(a[mid] = m\) then

7return \(mid\)// Elemento trovato

8end

9if \(a[mid] < m\) then

10\(left\) \(\leftarrow\) \(mid + 1\)// Cerca nella metà destra

11end

12else

13\(right\) \(\leftarrow\) \(mid - 1\)// Cerca nella metà sinistra

14end

15end

16return \(-1\)// Elemento non trovato

17end

Esegui in Colab:PythonC++Java

• L'invariante di ciclo del ciclo while di BinarySearch è:

Ogni volta che viene valutata la condizione alla riga 4:

• (I1) \(1\le left\) e \(right\le n\);

• (I2) se \(m\) è in \(a\), allora \(m\) è in \(a[left..right]\), cioè

  \[ m\in\{a[1],\dots,a[n]\} \ \Longrightarrow\ m\in\{a[left],\dots,a[right]\}. \]

• A parole: l'algoritmo non scarta mai una porzione dell'array che può contenere \(m\). Il sotto-array \(a[left..right]\) è detto intervallo di ricerca e contiene \(right-left+1\) elementi (è vuoto se \(left>right\)).

Esempio 13.4: Invariante di ciclo di BinarySearch

Ricerca di \(m=10\) in \(a=[3, 9, 11, 12, 12, 16, 19]\) (\(n=7\)). La tabella mostra l'intervallo di ricerca ogni volta che viene valutata la condizione alla riga 4.

\(left\)	\(right\)	\(a[left..right]\)	azione
1	7	\([3,9,11,12,12,16,19]\)	\(mid=4\), \(a[4]=12>10\) \(\Rightarrow\) \(right=3\)
1	3	\([3,9,11]\)	\(mid=2\), \(a[2]=9<10\) \(\Rightarrow\) \(left=3\)
3	3	\([11]\)	\(mid=3\), \(a[3]=11>10\) \(\Rightarrow\) \(right=2\)
3	2	\([\ ]\)	\(left>right\) \(\Rightarrow\) restituisce \(-1\)

Poiché \(10\) non è in \(a\), l'invariante (I2) è banalmente vero; quando l'intervallo diventa vuoto l'algoritmo restituisce correttamente \(-1\).

Osservazione 13.6

Dati un array \(a[1..n]\) di \(n\) numeri naturali ordinato in modo non decrescente e un numero naturale \(m\), l'algoritmo BinarySearch termina; restituisce un indice \(k\) tale che \(a[k]=m\) se \(m\) è in \(a\), e restituisce \(-1\) altrimenti.

Dimostrazione

Dimostriamo le tre proprietà dell'invariante di ciclo.

• Inizializzazione. Le righe 2 e 3 pongono \(left=1\) e \(right=n\). Allora (I1) vale, e \(a[left..right]=a[1..n]\) è l'intero array, quindi (I2) vale.

• Conservazione. Supponiamo che (I1)–(I2) valgano e che \(left\le right\). La riga 5 calcola \(mid=left+\lfloor(right-left)/2\rfloor\); poiché \(0\le \lfloor(right-left)/2\rfloor\le right-left\), si ha

  \[ 1\le left\le mid\le right\le n, \]

  quindi \(a[mid]\) è una componente valida dell'array. Sono possibili tre casi.

  • \(a[mid]=m\): l'algoritmo restituisce \(mid\) alla riga 7, che è un output corretto.

  • \(a[mid]<m\): poiché l'array è ordinato, per ogni \(k\le mid\) si ha \(a[k]\le a[mid]<m\). Quindi \(m\) non è in \(a[left..mid]\), e se \(m\) è in \(a[left..right]\) allora è in \(a[mid+1..right]\). La riga 10 pone \(left\leftarrow mid+1\ge 1\), quindi (I1) e (I2) valgono ancora.

  • \(a[mid]>m\): poiché l'array è ordinato, per ogni \(k\ge mid\) si ha \(a[k]\ge a[mid]>m\). Quindi, se \(m\) è in \(a[left..right]\), allora è in \(a[left..mid-1]\). La riga 13 pone \(right\leftarrow mid-1\le n\), quindi (I1) e (I2) valgono ancora.

• Terminazione. Consideriamo il numero di elementi dell'intervallo di ricerca, \(right-left+1\). Nel secondo caso il nuovo numero è \(right-mid\le right-left\), nel terzo caso è \(mid-left\le right-left\): in entrambi i casi diminuisce di almeno \(1\). Poiché il ciclo continua solo finché \(right-left+1\ge 1\), il ciclo termina dopo al più \(n\) iterazioni. L'algoritmo finisce in uno di due modi:

  • restituisce \(mid\) con \(a[mid]=m\), che è corretto;

  • la condizione \(left\le right\) è falsa, cioè l'intervallo di ricerca \(a[left..right]\) è vuoto. Poiché un sotto-array vuoto non contiene \(m\), per (I2) \(m\) non è in \(a\), e l'algoritmo restituisce correttamente \(-1\) alla riga 16.

  Quindi l'algoritmo è corretto.

□

13.5 Correttezza dell'algoritmo di Euclide

Dati due numeri naturali \(n, m \ge 1\), consideriamo il problema di calcolare il loro massimo comune divisore \(\gcd(n,m)\).

• Nell'ultimo esempio l'invariante non è una proprietà di una porzione di un array, ma un'uguaglianza fra due numeri che non cambia mai. Questo è lo pseudocodice dell'algoritmo di Euclide.

Algoritmo: EuclideanAlgorithm

Input: Due numeri naturali \(n, m \ge 1\)

Output: \(\gcd(n, m)\)

1function EuclideanAlgorithm(\(n\), \(m\))

2while \(m \ne 0\) do

3\(r := n \bmod m\)

4\(n \leftarrow m\)

5\(m \leftarrow r\)

6end

7return \(n\)// \(m = 0\): \(n\) è il MCD

8end

Esegui in Colab:PythonC++Java

• La dimostrazione si basa sulla seguente proprietà del massimo comune divisore, dimostrata nel capitolo «Algoritmi numerici»:

  \[ \gcd(n, m) = \gcd(m,\ n \bmod m)\qquad \text{per ogni } n\ge 1,\ m \ge 1. \]

• Usiamo anche la convenzione \(\gcd(n,0)=n\) per \(n\ge 1\): ogni numero naturale divide \(0\), quindi i divisori comuni di \(n\) e \(0\) sono i divisori di \(n\), e il più grande di essi è \(n\).

• Indichiamo con \(n_0\) e \(m_0\) i valori di \(n\) e \(m\) dati in input. L'invariante di ciclo del ciclo while è:

Ogni volta che viene valutata la condizione alla riga 2, \(n\ge 1\), \(m\ge 0\), e

\[ \gcd(n,m)=\gcd(n_0,m_0). \]

Esempio 13.5: Invariante di ciclo dell'algoritmo di Euclide

Consideriamo \(n_0=252\) e \(m_0=105\). La tabella mostra i valori di \(n\) e \(m\) ogni volta che viene valutata la condizione alla riga 2:

\(n\)	\(m\)	\(\gcd(n,m)\)
252	105	21
105	42	21
42	21	21
21	0	21 (il ciclo termina)

Il valore \(\gcd(n,m)=21\) non cambia mai, e quando \(m=0\) l'algoritmo restituisce \(n=21=\gcd(252,105)\).

Osservazione 13.7

Dati due numeri naturali \(n_0,m_0\ge 1\), l'algoritmo EuclideanAlgorithm termina e restituisce \(\gcd(n_0,m_0)\).

Dimostrazione

Dimostriamo le tre proprietà dell'invariante di ciclo.

• Inizializzazione. Prima della prima iterazione \(n=n_0\ge 1\) e \(m=m_0\ge 1\), quindi banalmente \(\gcd(n,m)=\gcd(n_0,m_0)\).

• Conservazione. Supponiamo che l'invariante valga e che \(m\ne 0\), cioè \(m\ge 1\). La riga 3 calcola \(r=n\bmod m\), con \(0\le r<m\). Le righe 4–5 sostituiscono la coppia \((n,m)\) con \((m,r)\). Il nuovo valore di \(n\) è \(m\ge 1\), il nuovo valore di \(m\) è \(r\ge 0\), e, poiché \(n,m\ge 1\),

  \[ \gcd(m,r)=\gcd(m,\ n\bmod m)=\gcd(n,m)=\gcd(n_0,m_0). \]

  Quindi l'invariante vale prima dell'iterazione successiva.

• Terminazione. A ogni iterazione il valore di \(m\) viene sostituito da \(r<m\), quindi \(m\) è un numero naturale che diminuisce strettamente. Quindi il ciclo termina dopo al più \(m_0\) iterazioni, quando \(m=0\). Sostituendo \(m=0\) nell'invariante di ciclo otteniamo

  \[ \gcd(n_0,m_0)=\gcd(n,0)=n, \]

  che è il valore restituito alla riga 7. Quindi l'algoritmo è corretto.

□

• La dimostrazione non usa l'ipotesi \(n_0\ge m_0\): se \(n_0<m_0\), allora \(n_0\bmod m_0=n_0\) e la prima iterazione si limita a scambiare i due numeri.

• Il limite “al più \(m_0\) iterazioni” basta a dimostrare la terminazione, ma è molto pessimistico: il numero di iterazioni è in realtà \(O(\log_2 m_0)\) (nell'esempio, \(3\) iterazioni per \(m_0=105\)).

13.6 Correttezza degli algoritmi ricorsivi

• Gli invarianti di ciclo sono lo strumento per dimostrare la correttezza degli algoritmi iterativi, cioè basati su cicli.

• Un algoritmo ricorsivo risolve un'istanza di un problema chiamando se stesso su una o più istanze più piccole. La sua correttezza si dimostra direttamente per induzione matematica sulla dimensione dell'istanza:

  • caso base: l'algoritmo restituisce l'output corretto sulle istanze più piccole, che sono risolte senza chiamate ricorsive;

  • passo induttivo: sotto l'ipotesi induttiva che le chiamate ricorsive restituiscano l'output corretto sulle istanze più piccole, l'algoritmo ne combina i risultati nell'output corretto per l'istanza corrente.

• La terminazione segue dal fatto che ogni chiamata ricorsiva è fatta su un'istanza strettamente più piccola, quindi prima o poi si raggiunge il caso base.

La correttezza degli algoritmi ricorsivi si dimostra per induzione sulla dimensione dell'input. Questa tecnica viene applicata insieme allo studio degli algoritmi ricorsivi.

Punti chiave del capitolo

• Un algoritmo è corretto se, per ogni istanza di input, termina e restituisce l'output corretto; i test possono solo mostrare che un algoritmo è sbagliato.

• La correttezza di un ciclo si dimostra con un invariante di ciclo: inizializzazione, conservazione e terminazione.

• L'invariante, insieme alla negazione della condizione del ciclo, fornisce l'output: \(i=n+1\) per Find Maximum e Insertion Sort, un intervallo di ricerca vuoto per Binary Search, \(m=0\) per l'algoritmo di Euclide.

• I cicli annidati richiedono un invariante per ciascun ciclo (Insertion Sort); un return dentro il ciclo è una seconda uscita che va dimostrata corretta (Binary Search).

• Gli algoritmi ricorsivi si dimostrano corretti per induzione sulla dimensione dell'input.

---

Esercizi su questo capitolo: Correttezza

Laboratorio interattivo

L'algoritmo del capitolo, un passo alla volta: muovi i cursori e premi ▶. Lo stesso grafico a tutta pagina, con gli altri del corso, è nel laboratorio interattivo.