Da dove viene il vantaggio della programmazione strutturata rispetto alla programmazione più libera? Dov’è la logica che togliere libertà aggiunge potenza?

Ebbene è proprio una questione di logica: nella programmazione strutturata si riescono a dare dei significati logico - matematici ad ogni istruzione, cosa assolutamente impossibile con una programmazione libera.

Il modo più semplice per spiegare una istruzione è dare la sequenza di operazioni che vengono svolte per realizzarla. In questo caso parleremo di semantica operazionale; cioè la semantica, il significato dell’istruzione, viene data attraverso delle operazioni.

Prendiamo un piccolo spezzone di codice:

if x > 0 then

x := -x;

e diamone un significato operazionale: il processore arriva all’istruzione if e controlla il valore della variabile x, se è maggiore di zero memorizza il valore di x cambiato di segno nella variabile x stessa.

Chi legge in questo modo uno spezzone di codice immagina di eseguire una per una le istruzioni che incontra, simula quello che farà il computer e quindi capisce o intuisce il risultato finale.

Ma c’è un modo completamente diverso di vedere un programma: dare una semantica assiomatica, cioè legare delle proprietà logiche ad ogni punto del programma e definire per ogni operazione come queste proprietà si modificano.

Con questa visione lo spezzone di programma diventa:

{ x>=0 or x<0 }

if x<0 then

{ x< 0 }

x := -x;

{ -x <0 } che implica { x>=0 }

{ x >= 0 }

Leggiamolo in dettaglio.La prima riga esprime un proprietà logica della variabile x: può essere maggiore uguale a zero oppure minore di zero.Il nostro fine è arrivare ad avere x maggiore o uguale a zero, come viene espresso dall’ultima riga del programma.

Nella seconda riga incontriamo ora una istruzione IF. Da punto di vista logico, se la condizione dell’IF è falsa dobbiamo poter dedurre senza l’intervento di nessun’altra istruzione la postcondizione direttamente dalla precondizione.

In questo caso che da

{ ( x>=0 or x<0 ) and not( x<0 ) }

che sono la precondizione e la negazione del test dell’IF si deve poter dedurre

{ x>=0 }

Ma la deduzione è semplicissima, in quanto è proprio la precondizione che dice che x è non minore di zero.

Se il test è falso invece viene eseguita l’istruzione di assegnazione della quarta riga. In questo caso abbiamo una affermazione sulla variabile x che dobbiamo sfruttare combinata con l’espressione che viene assegnata per derivare le proprietà logiche valide dopo l’assegnazione. Alla quinta riga troviamo il risultato di queste considerazioni.

E’ molto interessante notare come la postcondizione sia la stessa percorrendo entrambe le strade: partendo da {x>=0 or x<0} si arriva in ogni caso a {x>=0}. Dal punto di vista assiomatico l’istruzione IF non divide due percorsi, ma anzi rende vera una proprietà comune!

Ogni istruzione strutturata ha una definizione assiomatica del proprio comportamento.

Vediamo le principali.

Assegnazione { P(w)} v:=w { P(v) }

Sequenza

Premesse: { P } I1 { C } , { C } I2 { R }

Conseguenza: { P } I1 I2 { R }

Istruzioni condizionali

premesse: { P and D } I1 { C } , { P and not(D) } I2 { C }

conseguenza: { P } if D then I1 else I2 { C }

Istruzioni ripetitive

premesse: { P and D } I { P }

conseguenza: { P } while D do I { P and not(D) }

E’ interessante notare come questa visione indica che l’istruzione IF unifica una proprietà logica e l’istruzione WHILE ha una proprietà che non varia durante tutto il ciclo (invariante ciclico), esattamente il contrario di quello che viene evidenziato dalla semantica operazionale!

Con questi metodi è possibile dimostrare matematicamente la correttezza di ogni programma strutturato, anche se purtroppo è talmente complesso da non essere un procedimento effettivo per applicazioni del mondo reale.

Possiamo fare un paragone con il lavoro dell’ingegnere edile: le case sicuramente stanno in piedi per le regole della gravitazione universale formulate da Newton, ma mai e poi mai i calcoli del cemento armato si fanno con F=MA, perchè sarebbe lungo e dispendioso. Si ricorre a tabelle e formulari, in cui la legge è già applicata a travi e colonne delle più svariate forme più una buona dose di buon senso e di sicurezza calcolando i carichi per eccesso.

L’ingegnere del software si trova quasi nella stessa situazione: una regola generale esiste, ma non sono stati ancora sviluppati i formulari perchè possa essere applicata direttamente in casi reali. Ma l’esistenza di queste regole dimostra la possibilità di costruire un "manuale del programmatore", in cui siano contenute le indicazioni rapide per giungere a programmi rispondenti alle specifiche e privi di errori.