Per verificare la correttezza di un programma informatico, spesso ci si limita a provarlo con una batteria di test, ma ciò è sufficiente solo se si esaminano tutti i casi possibili! Prima di arrivare a questa fase, conviene fondare il programma sulla sua dimostrazione. In realtà, il problema si pone solo nel caso dei cicli iterativi o ricorsivi.
Riferimenti
La logique. Bibliothèque Tangente 15, 2004.
Mathématiques et informatique. Bibliothèque Tangente 52, 2014.
Les démonstrations. Bibliothèque Tangente 55, 2015.

Suite à 11 (18). Bernard Frize, 2006.

-
Più delicato: il caso delle funzioni iterative ----------------------------------------------
In genere è più difficile dimostrare che un programma fornisce il risultato atteso per una funzione iterativa (cioè strutturata attorno a un ciclo come «ripeti», «finché» o «per») che per una funzione ricorsiva. Le dimostrazioni si fondano sulla nozione di invariante di ciclo.
Consideriamo il calcolo dell’MCD (massimo comune divisore) di due numeri con l’algoritmo di Euclide. L’idea luminosa attribuita a Euclide consiste nell’osservare che l’MCD di due numeri a e b è lo stesso di a e b modulo a, cioè del resto d della divisione euclidea di a per b. Si ha allora il seguente programma in pseudocodice:
MCD(a,b)=
Si introduce una variabile supplementare d
Ripeti
d:=a mod b
a:=b
b:=d
fino a quando d=0
restituisci a
L’invariante di ciclo è: «I divisori comuni di a e b sono gli stessi a ogni passaggio.» Inoltre, la successione dei valori di d è strettamente decrescente, il che garantisce l’uscita dal ciclo. Questo algoritmo può essere formulato in forma ricorsiva:
MCDRic(a,b)=
Se a=0, restituisci b
Altrimenti restituisci MCDRic(b mod a, a)
Questo programma si dimostra allora senza difficoltà per induzione sul numero intero a.
-
Programmare significa dimostrare: il caso delle funzioni ricorsive -----------------------------------------------------------
Il corpo di una funzione ricorsiva comprende in genere due parti: il trattamento del caso base e la parte propriamente ricorsiva, da accostare al ragionamento per induzione. L’esempio classico è il calcolo del fattoriale di un numero intero positivo. Ecco un esempio in pseudocodice:
Fattoriale(n)=
Se n=0, restituisci 1
Altrimenti restituisci n\*Fattoriale(n-1)
La dimostrazione che la funzione Fattoriale restituisce effettivamente il prodotto di tutti gli interi da 1 a n (indicato con n!) per ogni numero naturale n si ottiene per induzione. La dimostrazione si fa leggendo le righe del programma precedente. Formalizziamo il ragionamento considerando P(n) come la proprietà «Fattoriale(n) restituisce n!».
P(0) è vera in base alla prima riga del programma. Supponiamo ora che P(n–1) sia vera per un numero intero n ≥ 1 ed esaminiamo P(n). Fattoriale(n) richiama Fattoriale(n-1) che, per l’ipotesi induttiva, restituisce (n–1)! La seconda riga del programma restituisce dunque n×(n–1)!, che vale n!, quindi P(n) è vera. Così, P(0) è vera e, se P(n–1) è vera, lo è anche P(n). Per il principio di induzione, P(n) è dunque vera per ogni numero naturale n.
In realtà, questa dimostrazione segue esattamente la programmazione della funzione. Possiamo riassumere affermando che, in questo caso, programmare significa dimostrare!