Premessa

Ovviamente sto parlando di informatica.
Partiamo dall'inizio: perché sto scrivendo questo articolo? Perché Giovedì prossimo dovrò dare l' esame di "Programmazione 1" e quindi questo articolo serve a me come ripasso. Resta comunque il fatto che l' argomento mi ha incuriosito o, per dirla tutta, non avrei mai immaginato di dover trattare dei semplici, banali e, se vogliamo, scontati argomenti di programmazione con il linguaggio della matematica.
Prima di allora vedevo la programmazione come un qualcosa di dinamico e la matematica statica, ma non è così. I due linguaggi sono in relazione.

Dove si applicano

In generale nelle funzioni (o metodi, chiamiamoli come meglio ci pare), in particolare nei cicli. L' idea che sta alla base di tutto è riuscire a trovare un metodo matematico per capire a priori se un qualcosa funziona senza bisogno di farlo "girare" su di una macchina.
Inizialmente la cosa mi sembrava bizzarra, per dirla utilizzando un'espressione tipica dell'Africa sub sahariana, una "sega mentale". Inutile dire che mi sono dovuto ricredere. Non tanto perché la cosa funziona davvero (ho avuto modo di sperimentarla in una funzione su cui sto lavorando) ma per l' estrema teorizzazione.

Le idee di base per la correttezza parziale

Sono sostanzialmente due: l' utilizzo di un predicato invariante e l' applicazione del principio di induzione logica. Si applicano al corpo di un ciclo, a quello che succede all'interno di un ciclo ma, con opportuni trucchetti si possono applicare alla funzione/metodo generale. Direi che la cosa migliore sia partire dall'analisi di quello che succede all'interno di un ciclo.
Possiamo iniziare prendendo come esempio un metodo classico ed anche estremamente semplice,per non dire banale: la somma di due numeri ottenuta mediante incrementi successivi. Per ottenere la somma s = x + y senza avere a disposizione l' operazione binaria di somma, si può ottenere il risultato partendo con l' assegnare ad s il valore di x ed eseguire un ciclo che, ad ogni passaggio, incrementa il valore d s e decrementa il valore di y fino a quando y raggiunge il valore 0.
Prendiamo quindi come esempio il seguente metodo statico scritto in Java che calcola la somma di due numeri interi e positivi ed analizziamolo:

public static int somma (int x, int y) {
  int s = x;
  int n = y;
  // Punto A
  while (n > 0) {
    // Punto B
    s = s + 1; // accumula il risultato in s
    n = n - 1;
    // Punto C
  }
  // Punto D
  retun s;
}

Questo esempio può essere utile per capire il concetto.

Predicato invariante

L' idea è quella di formulare un predicato, un' espressione, una proprietà che valga in ogni punto della funzione. Ragionevolmente questa proprietà dovrebbe coinvolgere le variabili presenti nella funzione altrimenti non avrebbe senso. Nel caso in esame si potrebbe affermare (in modo semplificato) che:

Questa proprietà viene chiamata invariante proprio perché deve essere sempre verificata. Vediamo se è così nei vari punti del metodo.

Punto A

In questo punto ci troviamo nella condizione in cui

s = x

n = y

e quindi è ovvio che

s = x + y − n

Ed è facile verificarlo assegnando due valori a caso. Supponiamo che i parametri attuali siano 23 e 45, la nostra espressione diventa

23 = 68 − 45

Ed è verificata.

Punto B

Innanzi tutto, se siamo arrivati in questo punto è perché n > 0 quindi, per semplicità, supponiamo di essere appena entrati nel ciclo. Ovviamente essendo al primo ciclo la condizione è verificata. La cosa interessante è vedere se l' invariante è ancora vero alla fine delle operazioni che si svolgono all'interno del ciclo. Passiamo quindi al punto successivo.

Punto C

Arrivati a questo punto dobbiamo chiederci cosa sono diventate le variabili che compaiono nell' espressione. In buona sostanza dobbiamo vedere cosa è cambiato e come è cambiato, sostituire questi cambiamenti nell'espressione e verificare che sia ancora vera.

x,y sono sempre le stesse

s = s + 1

n = n − 1

Sostituendo questi nuovi valori nell' espressione otteniamo

(s + 1) = x + y − (n − 1)

s + 1 = x + y − n + 1

s = x + y − n + 1 − 1

s = x + y − n

Anche nella sua forma l'espressione non è cambiata, è sempre la stessa. Per adesso possiamo dire che questo predicato è davvero invariante. Manca solo la prova finale.

Punto D

Se siamo usciti dal ciclo è perché n = 0 e, visto che effettivamente il programma ha fatto quello che doveva fare in s avremo effettivamente il risultato della somma fra x e y quindi:

s = x + y + 0

Quindi possiamo dire che l' espressione s = x + y − n che abbiamo scelto per la verifica è davvero un invariante! Se ci fossimo dimenticati di incrementare s ce ne saremmo accorti perché l' invariante sarebbe .... variato, e quindi la verifica di correttezza sarebbe andata a pallino.

Induzione logica

Il principio di induzione logica è una di quelle cose che non conoscevo. L' ho studiata volentieri anche perché c'è stato un momento che tre professori di tre materie diverse ci hanno messo sotto il fuoco incrociato: tutti la spiegavano (ognuno secondo la sua sensibilità) e quindi, volente o nolente, l' ho imparato. Devo dire che è un principio potente e mi hanno detto che è una tecnica di dimostrazione molto importante. In questo caso la si può applicare per la verifica di correttezza dei programmi.
In estrema sintesi questo principio serve per verificare che un'espressione, una proprietà in genere, sia valida per ogni valore e si basa su questa idea. Supponiamo di avere una qualsiasi formula o proprietà che dipende da un numero n. Prendiamo come esempio questa espressione. :

Supponiamo ora che vogliamo dimostrare che la formula è giusta e che vale per qualsiasi valore di n
Il principio d' induzione in pratica dice che (lo dico malamente, da manovale, non me ne vogliano i puri) "Supponiamo che la formula sia corretta per un n qualsiasi. Se vale per il valore 0, e se vale per un n qualsiasi (cosa che supponiamo appunto vera) e per il suo successivo (n + 1) allora possiamo dire che vale per qualsiasi numero k". Cioè:

A questo punto, prima di implementarla, possiamo utilizzare il principio d'induzione su n per dimostrare che quella formula è vera, che veramente il quadrato di un numero corrisponde a quella sommatoria.
Iniziamo con il dimostrare la base, cioè il punto di partenza, la P(0). In questo caso, visto che la sommatoria va da 1 ad n dimostriamo per i = 1 in tal caso.

OK, è verificata.

Supponendo che la formula sia valida, quindi vale P(n) verifichiamolo per P(n + 1)

se

allora

ma l' ipotesi induttiva ci dice che possiamo sostituire la sommatoria con n², otteniamo così

(n + 1)² = 2(n + 1) − 1 + n²

n² + 2n + 1 = 2n + 2 − 1 + n²

n² + 2n + 1 = n² + 2n + 1 ed è verificata anche questa.

Questo principio si può utilizzare anche con la programmazione, il metodo seguente ne è una possibile implementazione.

public static int square(int x) {
  int qn = 0;
  int n = 1;
  // Base
  while((n <= x)) {
    qn = qn + 2 * n - 1;
    n = n + 1; 
  }
  return qn;
}

Per usare il principio d'induzione dobbiamo anche qui definire un invariante. La variabile qn è utilizzata per accumulare il risultato e l' induzione dobbiamo farla riferita ai cicli, al k − esimo ciclo. Direi che questo potrebbe andare bene per specificare quanto vale qn al k − esimo ciclo

(ipotesi induttiva)

Dobbiamo ora verificare che il predicato sia vero prima di entrare nel ciclo, cioè verificare la cosiddetta base al punto indicato nel sorgente. Questo serve anche per essere sicuri di aver inizializzato le variabili in modo corretto. Indichiamo come qn₀ e n₀ i valori delle variabili al passo 0.

qn₀ = 0

n₀ = 1

OK,la base è verificata.

Dopo k cicli, al (k + 1) − esimo ciclo, l' invariante sarà

Per verificarlo dobbiamo tenere presente che al ciclo k + 1 abbiamo

n_{k + 1} = n_k + 1 , in altre parole n_k = n_{k + 1} − 1 questo ci servirà più avanti.

Al ciclo k + 1 quanto vale qn_{k + 1}?
qn_{k + 1} = qn_k + 2n_k − 1
Ma per l' ipotesi induttiva
quindi

cioè
E quindi è verificato. Ora vediamo se l' invariante è davvero un invariante anche all' uscita del ciclo. Come si vede dal sorgente il ciclo termina quando n = x ma l' ultima operazione che il ciclo fà è quella di incrementare n quindi avremo che n = n + 1. Applicando l' invariante otteniamo

Che è quello che volevamo ottenere dal metodo. Inoltre abbiamo anche dimostrato la correttezza perché l' invariante è davvero invariante e vale in tutti punti del metodo: prima del ciclo, durante il ciclo ed alla fine del ciclo.

Versione ricorsiva

L'esempietto appena analizzato può essere anche implementato in forma ricorsiva. Personalmente trovo la ricorsione un modo estremamente elegante per scrivere programmi. Purtroppo esclusi alcuni casi in cui non se ne può fare a meno, le implementazioni ricorsive sono poco efficienti, consumano una quantità vergognosa di stack.
Nell' esempio si dice alla macchina "Parti con n=1, esegui un ciclo dentro il quale aggiungi al risultato quello che ti dico io, ad ogni giro incrementi n, e continua a farlo fino a quando n<=x".
L' implementazione ricorsiva è diversa. Nel nostro caso potremmo ragionare in questo mdo: "Se l' argomento è 0 il risultato vale 0, in tutti gli altri casi il risultato vale (x − 1)² + 2x − 1 cioè il quadrato del numero precedente più 2x − 1". Fine della storia.
La cosa affascinante è che il programma si scrive nello stesso modo in cui si descrive il ragionamento.

public static int square(int x) {
  if (x == 0) return 0;
  else return square(x - 1) + 2 * x - 1;
}

Non abbiamo contatori, non abbiamo cicli, c'è solo il ragionamento puro e semplice.
Un modo ragionevole per dimostrare la correttezza parziale sarebbe semplicemente dimostrare l' equazione scritta nella seconda linea di codice, cioè

x² = (x − 1)² + 2x − 1

E lo si può dimostrare per induzione su x. Anche volendo non potremmo farlo sui cicli (con il k dell'esempio di prima) semplicemente perché ... non c'è nessun ciclo. In buona sostanza si tratta di fare una dimostrazione matematica su una formula matematica.

Base

La prima riga del programma ci dice già di suo che con x = 0 in suo quadrato vale 0. Verificato.

Passo induttivo

L' ipotesi induttiva che prendiamo per vera è la formula stessa. Verifichiamo che sia vera anche per x + 1

(x + 1)² = ((x + 1) − 1)² + 2(x + 1) − 1

x² + 2x + 1 = x² + 2x + 2 − 1

x² + 2x + 1 = x² + 2x + 1

Fine della dimostrazione.

L'idea di base per la terminazione

Un ciclo, un algoritmo in generale deve prima o poi terminare. Da quello che ho capito io nelle lezioni (e spero di aver capito giusto altrimenti all'esame saranno volatili per diabetici) l' idea è quella di fare in modo che ci sia un qualcosa che "assomigli" all'insieme dei numeri naturali perché questo ha un minimo che è 0 al di sotto del quale non si può andare. Quindi, nel caso di un ciclo, anche qui bisogna formulare un invariante il cui valore, ad ogni ciclo, sia strettamente minore del ciclo precedente. Nell'esempio di prima, quello iterativo, abbiamo la variabile b che aumenta invece che diminuire, quindi un invariante ragionevole potrebbe essere

x − b_k

E verificare per induzione sul numero dei cicli k che il valore al (k + 1) − esimo ciclo sia strettamente minore del valore che avrebbe al k − esimo ciclo

Base

La base dell' induzione sta nel dimostrare che il valore al ciclo k₁ sia minore del valore che si ha al ciclo k₀. Dal sorgente vediamo che, dopo il primo ciclo

n_k1 = n_k0 + 1

quindi

b − (n_k0 + 1) < b − n_k0

b − n_k0 − 1 < b − n_k0 OK, verificato!

Passo induttivo

Prendiamo come ipotesi induttiva, cioè che sia vero che

x − b_{k + 1} < x − b_k

Quindi il passo induttivo sarà

L' antecedente dell' implicazione lo abbiamo già assunto come vero, se dimostriamo che il conseguente è vero allora tutto l' ambaradan varrà per qualsiasi valore di k

x − b_{k + 2} = x − (b_{k + 1} + 1) = x − b_{k + 1} − 1

Sostituendo il valore ottenuto

x − b_{k + 1} − 1 < x − b_{k + 1}

In base a questa dimostrazione possiamo dire che esiste di sicuro un k tale che

Questo vuol dire che si arriverà sicuramente in un punto dove il valore di b sarà uguale o supererà x quindi il ciclo di terminerà.

Conclusione

Ok, ho fatto il mio ripasso e quindi questo articolo mi ha impegnato a fare le cose per bene, soprattutto mi è servito a dissipare ancora qualche piccolo dubbio. Quindi direi che il risultato l' ho ottenuto.
C'è una cosa che però vorrei dire: non avrei mai e poi mai immaginato di fare una sorta di "analisi logica" ai programmi. In effetti professore ci ha sempre detto "se l' analisi logica si fa sulle frasi, perché non si può fare sui programmi?".
In effetti non è che quando parliamo o scriviamo pensiamo all'analisi logica delle frasi che diciamo, la sappiamo fare e direi anche che è un bene. Ed allora è bene saperla fare anche sui programmi.
La cosa che ho trovato più interessante in questo corso è stato l' uso massiccio della ricorsione. In tanti anni di lavoro ho letto parecchi libri e manuali di programmazione, e più o meno tutti portano il solito esempio del calcolo del fattoriale scritto in modo ricorsivo. Insomma, sempre la solita minestra.
Per carità, mi è anche capitato di scrivere degli analizzatori sintattici e più di un compilatore ma ho sempre visto la ricorsione come un male necessario, mai come un modo bello, elegante per scrivere programmi o, per dirla meglio, per trasportare direttamente un ragionamento in un programma.