La specifica di un programma è l’espressione non ambigua dei requisiti che un committente impone al programma che intende far costruire.
I requisiti sono di due tipi:
- requisiti di efficienza e di ambiente, quali il tempo di risposta, le limitazioni di memoria, l’utilizzo di particolari risorse hardware o software, ecc.
- requisiti funzionali che esprimono la relazione funzionale
che deve valere tra i valori di input sottoposti al programma e i valori
di output ritornati dallo stesso.
Nell’ambito delle relazioni tra specifiche e correttezza programmi ciò che segue intende essere una breve introduzione alla correttezza dei programmi solo dal punto di vista dei requisiti funzionali.
1. Definizioni
Un programma realizza una relazione funzionale tra i valori di input e quelli di output.
Se astraiamo dal modo in cui un programma ottiene l’output, il suo effetto può essere rappresentato dalla sua astrazione funzionale come insieme di coppie F = {(s, s’)} in cui per ogni s esiste una e una sola coppia (s, s’).
Ad esempio l’astrazione funzionale di un programma che calcola il quadrato di un numero naturale è l’insieme di coppie {(0, 0), (1, 1), (2, 4), (3, 9), (4, 16) . . . } .
Per assicurare che un programma soddisfi la sua specifica occorre definire l’insieme di coppie "corrette" e dimostrare che l’astrazione funzionale del programma coincide con tale insieme, cioè che il programma, avendo in input il primo elemento di una qualunque coppia "corretta", restituisce in output il secondo elemento della coppia stessa.
Poichè in generale la funzione che deve essere calcolata da un
programma è un insieme di coppie infinito, anzichè specificare
l’insieme delle coppie, si usano i predicati della logica per caratterizzare
le coppie di input/output che si devono ottenere. Riprendendo l’esempio
precedente si può caratterizzare l’insieme di coppie { (0, 0), (1,
1), (2, 4), (3, 9), (4, 16) . . . }come:
{(x, z) / x Î N & z = x *
x }
1.1. Specifica di un programma
Dato un programma P, con variabili di input x1, x2, . . . , xn ( x ) e variabili di output z1, z2, . . . ,zk ( z ), si chiama specifica di P la coppia di predicati: < j ( x ), y ( x, z )>, dove:
- j ( x ), detto predicato di input di P, specifica i vincoli cui devono soddisfare i valori forniti per le variabili (il dominio delle variabili);
- y ( x, z ), detto predicato
di output di P, specifica la relazione di input / output.
Ad esempio, se P è un programma che calcola il quadrato di un numero naturale, nell’ipotesi che x sia dicharata come variabile intera, poichè i naturali sono un sottinsieme degli interi, in particolare gli interi maggiori o uguali a zero, P avrà come predicato di input j ( x ) º x ³ 0 e come predicato di output y ( x, z ) º z = x * x.
Come altro esempio consideriamo il programma Q che, dati due interi non negativi x1 e x2, con x2 diverso da zero, calcola il quoziente e il resto della divisione di x1 per x2:
j ( x1, x2 ) º x1 ³ 0 & x2 > 0
y ( x1, x2, z1, z2 ) º x1 = z1 * x2 + z2 & 0 £ z2 < x2.
Il predicato di output esprime la nota relazione: il dividendo (x1)
è uguale al divisore (x2) per il quoziente (z1) più il resto
(z2) ed il resto è maggiore o uguale a 0 e minore del divisore.
1.2. Correttezza parziale
Dato un programma P e una specifica < j ( x ), y ( x, z )>, P si dice parzialmente corretto rispetto alla specifica se per ogni valore x delle variabili di input x, che soddisfa il predicato di input, se il programma termina con valore z per le variabili di output z, il predicato y ( x , z ) è soddisfatto:
" x : (j
(x ) & P(x
) ß zÞ
y ( x , z
) )
1.3. Terminazione
Dato un programma P e un predicato di input j ( x ), si dice che P termina su j ( x ) se per ogni valore x delle variabili di input x, che soddisfa il predicato di input, il programma P termina (denotato da Pß ):
" x : (j (x ) Þ P(x ) ß )
1.4. Correttezza totale
Dato un programma P e una specifica < j ( x ), y ( x, z )>, P si dice totalmente corretto rispetto alla specifica se per ogni valore x delle variabili di input x, che soddisfa il predicato di input, il programma termina con valore z per le variabili di output z, che soddisfa il predicato di output:
" x : (j
(x ) Þ
P(x ) ßz
& y ( x
, z ) )
1.5. Proprietà
Un programma P è totalmente corretto rispetto alla specifica
< j ( x ), y
( x, z )>, se e solo se è parzialmente corretto rispetto
a < j ( x ), y
( x, z )> e termina su j ( x
).
2. Verifica della correttezza
Per analizzare una tecnica di verifica della correttezza ci limitiamo alla classe dei programmi strutturati, realizzati con un insieme ristretto di strutture di controllo.
L’insieme minimo di strutture di controllo comprende, come è
noto, la sequenza, la selezione (ifthenelse) e l’iterazione (while
o repeat, a cui spesso viene aggiunto il for).
2.1. Programmi strutturati
I programmi strutturati possono essere definiti ricorsivamente nel seguente modo:
- l’assegnazione y ¬ g(x, y) e il programma vuoto null sono programmi strutturati;
- se P1 e P2 sono programmi strutturati e t(x, y) è un’espressione booleana, allora i seguenti sono programmi strutturati:
P1 ; P2
if t(x, y) then P1 else P2
while t(x, y) do P1
2.2. Correttezza parziale dei programmi strutturati
Dato un programma P, nel seguito, oltre a chiamare x il vettore delle sue variabili di input, che supporremo non modificato dalle istruzioni del programma, e z il vettore delle sue variabili di output, indicheremo con y1, y2, . . . ,ym (y) le variabili di programma, che non sono note all’esterno dello stesso.
Per questo motivo le variabili y non compaiono ne’ nel predicato di input ne’ in quello di output, che sono le uniche informazioni del programma note all’esterno, cioè le interfacce attraverso cui esso comunica con l’ambiente.
Per dimostrare la correttezza parziale dei programmi strutturati Hoare
ha introdotto la seguente notazione, detta formula di correttezza:
{p(x, y)} S {q(x,
y)}
dove p e q sono predicati e S un sottoprogramma. Il predicato p prende il nome di precondizione o condizione di input di S, il predicato q il nome di postcondizione o predicato di output di S.
Il suo significato è il seguente: se per i valori di x e y che soddisfano il predicato p(x, y) l’esecuzione di S termina, allora dopo l’esecuzione di S varrà il predicato q(x, y).
La correttezza parziale di un programma P rispetto alla specifica <j
, y > è espressa dalla formula di correttezza:
{ j ( x
)} P { y
( x, z )} .
2.3. Dimostrazioni di correttezza parziale
Data la formula di correttezza di un programma P: {j ( x ) } P { y ( x, z ) } , dimostrare che la formula è vera significa dimostrare la correttezza parziale di P.
Il programma P strutturato, se non è null o un’assegnazione,
può essere descritto come sequenza, selezione o iterazione di programmi
più semplici, a loro volta descrivibili come figure strutturate
composte da programmi ancora più semplici, e così via finchè
si troveranno, come programmi componenti delle strutture più interne,
gli statement elementari null o assegnazione.
Ad esempio, sia DIVISIONE il seguente programma:
S1 S3
S5 y1
¬
0
S6 S7 y2 ¬
x1
S8 while y2 ³
x2 do
S9 S10 y1 ¬ y1 +
1
S11 y2 ¬ y2 - x2
S4
q ¬ y1
S2
r ¬ y2
dove x1 e x2 sono le variabili di input e q ed r le variabili di output; y1 e y2 sono le variabili di programma. Il programma è la sequenza S1 ; S2. S1 = S3 ; S4, . . . ,S8 = while y2 ³ x2 do S9, . . . . S2, S4, S7, S10 e S11 sono statement elementari.
Questa idea di "sbriciolare" P in programmi sempre più semplici fino agli statement elementari, può essere applicata anche alla dimostrazione di correttezza "sezionando" di pari passo la dimostrazione della sua formula di correttezza : {j ( x )} P {y ( x, z )}.
Associamo perciò un assioma di correttezza ad ogni statement
elementare e una regola di correttezza ad ogni statement composto di sequenza,
selezione e iterazione.
Assiomi:
(null) { p( x, y)}null
{ p( x, y)}
(ass) {q( x, g(x, y))}
y ¬ g(x, y) {q(
x,
y)}
L’assioma associato allo statement null, che non ha alcun effetto e può essere disegnato nel linguaggio dei flow-chart come freccia, esprime il fatto che se un predicato è vero, resta vero se i valori delle variabili non vengono modificati.
L’assioma associato allo statement d’assegnazione dice che il predicato
q(x, y) sarà verificato dopo l’assegnazione y ¬
g(x, y) se il predicato è verificato prima sui valori
che y assumerà; q( x, g(x, y)).
Le regole sono scritte nella forma di regole di inferenza:
P1 , P2 , . . . , Pn
_________________
P
che si interpreta nel modo seguente: P è vero se sono veri P1
, P2 , . . . , Pn, quindi la dimostrazione di P è trasformata nelle
n dimostrazioni di P1 , P2 , . . . , Pn.
Regole
{p( x, y)} S1 {r(
x,
y)} , {r(
x,
y)} S2 {q(
x, y)}
(seq)
______________________________________
{p( x, y)} S1 ; S2 {q(
x,
y)}
{p( x, y) & t(x, y)}
S1 {q(x, y)}
, {p( x, y) & not t(x,
y)}
S2 {q(
x, y)}
(ifthenelse)
________________________________________________________
{p( x, y)} if t( x,
y) then S1 else S2 {q( x,
y)}
{p( x, y) & t(x, y)}
S {p( x, y)}
(while)
_________________________________________
{p( x, y)} while
t(x, y) do S {q( x,
y)
& not t(x, y)}
Le tre regole riducono la dimostrazione di una formula complessa a dimostrazioni di formule più semplici:
- (seq) trasforma la dimostrazione di {p(x,
y)}
S1 ; S2 {q(x,
y)}
nelle due dimostrazioni
{p(x, y)}
S1 {r(x, y)}
e {r(x, y)}
S2 {q(x, y)}
, con l’introduzione di un predicato intermedio, postcondizione di S1 e
precondizione di S2.
- (ifthenelse) esprime il fatto che, perchè q sia vero
dopo l’if-then-else, q deve essere vero sia che venga
eseguito il ramo then, sia che venga eseguito il ramo else,
cioè:
{p(x, y) & t(x, y)}
S1 {q(x, y)}
e {p(x, y) & not t(x,
y)}
S2 {q(x,
y)}
- (while) Poichè dopo l’esecuzione del while sarà
vero not t(x, y), il predicato p(x, y) &
not
t(x, y) sarà vero dopo il while se, essendo
p(x, y) vero prima, p(x, y) resterà
vero indipendentemente dal numero di volte che il corpo S viene eseguito;
ciò è assicurato dalla dimostrazione di:
{p( x, y) & t(x, y)}
S {p(x, y)}
.
Il predicato p(x, y) viene detto invariante del while.
Le regole precedenti vengono completate con due regole ausiliarie, dette
regole
di conseguenza:
{p(x, y)} S {r(x,
y)
} , r(x, y) Þ
q(x, y)
(C1)
_______________________________
{p(x, y)} S {q(x,
y)}
p(x, y) Þ r(x, y)
, { r(x, y)}
S { q(x, y)}
(C2)
________________________________
{p( x, y)} S {q(
x,
y)}
Per dimostrare la correttezza parziale di un programma possiamo costruire un albero che ha come radice la formula di correttezza che si vuole provare, nel modo illustrato dal seguente esempio:
P: {j (x)}
S1 S3 y ¬
f(x)
S4
while t(x,y) do
S5 y ¬ h(x,y)
S2
z ¬ g(x,y)
{y (x,z)}
N.B. Per poter leggere correttamente la dimostrazione, la linea
tratteggiata deve essere completamente visibile su un'unica riga.
---------------------------------------------------------------------------------------------------------------------------------
p(x,y) & t(x,y) Þ p(x, h(x,y))
& t(x,h(x,y)) ,
{p(x, h(x,y)) & t(x, h(x,y))} y ¬
h(x,y) {p(x,y)}
____________________________________
{p(x,y) & t} S5 º
y ¬ h(x,y) {p(x,y)}
____________________________________
j (x) Þ
p(x,f(x)) ,
{p(x,y)} while
t(x,y) do S5 {p(x,y) & not
t} ,
{p(x,f(x))} S3 {p(x,y)}
p(x,y) & not t Þ y
(x, g(x,y)
__________________________
__________________________________
{j(x)}
S3 º y ¬
f(x) {p(x,y)}
, {p(x,y)}while
t(x,y) do S5 {y(x, g(x,y)}
__________________________________________________________
{j(x)} S1 º
S3 ; S4 {y(x, g(x,y)}
_________________________________________________________
{j (x)} S1 {y
(x, g(x,y)}
, {y
(x, g(x,y) )} S2 º
z ¬ g(x,y) {y(x,z)}
_______________________________________________________________________________________________
{ j (x)} P
º
S1; S2 { y (x,z)}
Se le tre implicazioni trovate sono vere, è vera la formula di
correttezza {j (x)}
P {y (x,z)} , cioè
P è parzialmente corretto rispetto a < j
(x), y (x,z) >.
Come esempio costruiamo la dimostrazione formale del programma DIVISIONE:
{ x1 ³ 0 & x2 > 0}
y1 ¬ 0
y2 ¬ x1
while y2 ³ x2 do
y1 ¬ y1 + 1
y2 ¬ y2 - x2
q ¬ y1
r ¬ y2
{ c }
Per leggere la dimostrazione, fate attenzione alla Dimensione della
pagina!
------------------------------------------------------------------------------------------------------------------------------------------------------------------+
N.B. Per rendere più leggibile la dimostrazione, introduciamo
la seguente notazione:
p[y/x] è abbreviazione per il predicato ottenuto da p sostituendo
sostituendo tutte le occorrenze di x in p con y.
Ad esempio: sia pc º (x1 = q *
x2 + r & 0 £ r < x2), allora p[y2/r]
º (x1 = q *
x2 +y2 & 0 £ y2 < x2).
b & y2 ³ x2 Þh
,
{hºd[(y1+1)/y1]} S10 º
y1 ¬ y1 + 1 {dºb[(y2-x2)/y2]}
_________________________________________
{b & y2 ³
x2} S10 º y1 ¬
y1 + 1 {b [(y2-x2)/y2]}
, {b[(y2-x2)/y2]} S11
º
y2 ¬ y2-x2 {b}
___________________________________________________________________________
{b & y2 ³
x2} S9 º S10 ; S11{b}
_______________________________________ ..
{b } while y2 ³
x2 do S9 {b & y2<x2} ,
{g º b
[x1/y2]} S7 º y2 ¬
x1 {b }
b & y2<x2 Þ a
(*)
j Þm
,
___________________________
_________________________________
{ mºg[0/y1]}
y1 ¬ 0 {g}
{g} S7 {b } ,
{b } while y2 ³
x2 do S9{a }
___________________
_________________________________________________
{j } S5 {g}
{g } S6 º S7
; S8 {a }
__________________________________________________________________________
{j } S3 º S5
; S6 {a }
, {aº(y[y2/r])[y1/q]}
S4 º q ¬
y1 {y [y2/r]}
__________________________________________________________________________________________________________________
{j } S1 º S3;S4
{
y [y2/r]}
, { y
[y2/r]} r ¬ y2 {y}
__________________________________________________________________________________________________________________________________________
{j º x1 ³
0 & x2 > 0} P º S1 ; S2 º
r ¬ y2 {y º
x1 = q * x2 + r & 0 £ r < x2}
(*) Poichè b &
y2<x2 Þ a, siamo
in grado di definire il predicato b
come indebolimento del predicato a,
in modo che, insieme con la condizione y2 <
x2 implichi a.Una
buona scelta si rivela essere bº
x1 = y1 * x2 + y2 &
0 £
y2.
Alle foglie dell’albero sono associati assiomi, veri per ipotesi, e le tre implicazioni in neretto:
b & y2 ³ x2 Þ h º (x1 = y1 * x2 + y2 & 0 £ y2 & y2 ³ x2) Þ (x1 = (y1+1) * x2 + (y2-x2) & 0 £ (y2-x2) )
b & y2<x2 Þa º (x1 = y1 * x2 + y2 & 0 £ y2 & y2 < x2) Þ (x1 = y1 * x2 + y2 & 0 £ y2 < x2)
j Þ mº (x1 ³ 0 & x2 > 0) Þ (x1 = 0 * x2 + x1 & 0 £ x1)
Essendo le implicazioni vere, il programma è dimostrato parzialmente
corretto rispetto alla specifica data.
2.4. Programmi annotati
L’albero di dimostrazione può essere per semplicità sostituito dal programma annotato.
Un programma totalmente annotato è un programma in cui fra uno statement e il successivo viene inserito, fra parentesi graffe, un predicato che è postcondizione per lo statement precedente e precondizione per lo statement successivo. La sequenza di due predicati indica che il primo deve implicare il secondo.
Il primo esempio viene riscritto come programma annotato nel modo seguente:
{x1 ³
0 & x2 > 0}
y1 ¬
0
{x1 ³
0 & x2 > 0 & y1 = 0}
y2 ¬
x1
{x1 ³
0 & x2 > 0 & y1 = 0 & y2 = x1}
{x1 =
y1 * x2 + y2 & y2 ³
0}
while y2 ³
x2 do
{x1 = y1 * x2 + y2 & y2 ³
0 & y2 ³ x2}
{x1 = (y1 + 1) * x2 + (y2 - x2) &
(y2 - x2) ³ 0}
y1 ¬ y1 + 1
{x1 = y1 * x2 + (y2 - x2) & (y2 -
x2) ³ 0}
y2 ¬ y2 - x2
{x1 =
y1 * x2 + y2 & y2 ³
0 & y2 < x2}
q ¬
y1
{x1
= q * x2 + y2 & y2 ³
0 & y2 < x2}
r ¬
y2
{x1
= q * x2 + r & 0 £
r < x2}
Non è sempre indispensabile annotare completamente il programma, è sufficiente evidenziare i predicati più significativi:
{j º (
x1 ³ 0 & x2 > 0)}
y1 ¬ 0
y2 ¬ x1
{p º (
x1 = y1 * x2 + y2 & y2 ³
0) }
while y2 ³ x2 do
{p & y2 ³ x2}
y1 ¬ y1 + 1
y2 ¬ y2 - x2
{ p}
{x1 = y1 * x2 + y2 & y2
³
0 & y2 < x2}
q ¬ y1
r ¬ y2
{y º (
x1 = q * x2 + r & 0 £
r < x2) }
Le implicazioni prima trovate per la dimostrazione di correttezza parziale si ottengono nel seguente modo:
j Þ p' , dove p' è ottenuto da p sostituendo 0 a y1 e x2 a y2;
p & y2 ³ x2 Þ p’’ , dove p’’ è ottenuto da p sostituendo y1 + 1 a y1 e y2 – x2 a y2;
p Þ y ’
, dove y ’ è ottenuto da y
sostituendo y1 a q e y2 a r.
Come altro esempio consideriamo il programma DISTANZA:
DISTANZA (G, s)
{j º ("
v ÎV: (color[v] = WHITE & d[v] = ¥
) & s ÎV)}
Q ¬ make_empty
color [s] ¬
GRAY
d[s] ¬
0
enqueue (Q,s)
{I º
(" w ÎV: w Î
Q Þ color[w] = GREY &
" w Î V: (color[w] = GREY or color[w]
= BLACK) Þ d[w] = d(s,w)
)}
(1) while not_empty (Q) do
C1
u ¬ head (Q)
(2) while c’è v Î
Adj[u] non considerato do
C2 if color [v] = WHITE
then color [v] ¬ GRAY
d[v] ¬ d[u] + 1
enqueue (Q, v)
color [u] ¬ BLACK
dequeue (Q)
{y
º (" v ÎV: color[v]
= BLACK Þ d[w] = d
(s,w) )}
In questo caso si dovrà dimostrare che j , attraverso le assegnazioni iniziali, rende vero I: {j} S1 {I} , che I viene mantenuto dal corpo del while (1), cioè {I} C1 {I} e che I Þ y .
Dimostrare {I} C1 {I} implica a sua volta dimostrare che I è
anche invariante del while (2), cioè che I è sempre vero
dopo l’assegnazione
u ¬ head (Q) e {I} C2 {I}
2.5. Il costrutto for
Possiamo aggiungere alla definizione di programma strutturato anche il costrutto for:
-Se P è un programma strutturato, il seguente è un programma strutturato
for i ¬ a to b do P
Per semplicità supponiamo che gli estremi a e b siano numeri
naturali, con a ³ b
e che il "passo" sia uno.
Anche al costrutto for può
essere associata una regola di correttezza, ma, per non complicare queste
brevi note, è sufficiente notare come il costrutto for sia
equivalente al seguente programma:
i ¬ a
while i < b do
P
i ¬ i + 1
2.6. Dimostrazioni di Correttezza Totale
La proprietà 1.5 permette di spezzare la dimostrazione di correttezza totale di un programma P rispetto alla specifica < j(x), y(x, z)> in due dimostrazioni:
Un insieme S spesso usato, è l'insieme N dei numeri naturali.
Dimostriamo, a titolo d'esempio, la terminazione dei due programmi introdotti nel paragrafo precedente (o, meglio, dei while in essi presenti).
Programma DIVISIONE:
while y2 ³
x2 do
y1 ¬ y1 + 1
y2 ¬ y2 - x2
L'espressione che possiamo utilizzare è y2. Inizialmente a y2
è assegnato x2 e la condizione di input assicura x2 ³
0, perciò y2
³ 0. Il corpo del while
modifica
y2 con y2 - x2, ma solo se y2 ³
x2,
mantenendo perciò y2 ³ 0.
Allora y2 assume valori in N.
Inoltre il suo valore diminuisce
in quanto a y2 viene sottratto x2, che la condizione di input assicura
maggiore di zero.
N.B. Mentre il while, e quindi il programma DIVISIONE, termina sul predicato x1 ³ 0 & x2 > 0, non si può dimostrare la sua terminazione sul predicato x1 ³ 0 & x2 ³ 0. Infatti, nel caso x2 = 0, y2 non assume valori decrescenti e y2 ³ x2 resterà sempre vero, impedendo la terminazione del ciclo.
Programma DISTANZA
(1) while not_empty (Q) do
u ¬ head (Q)
(2) while c’è v Î
Adj[u] non considerato do
if color [v] = WHITE
then color [v] ¬ GRAY
d[v] ¬ d[u] + 1
enqueue (Q, v)
color [u] ¬ BLACK
dequeue (Q)
Per la terminazione del while (2) si può considerare il numero di adiacenti ad u non ancora considerati, che diminuisce di 1, fino a 0, ad ogni esecuzione dello statement if-then (abbreviazione di if t then S else null ).
Dimostrare la terminazione del while (1) è più
complicato perchè bisogna dimostrare che la coda Q prima o poi sarà
vuota. Sappiamo che in Q vengono messi tutti e soli i vertici raggiungibili
dal sorgente s. Il numero di vertici raggiungibili da s, non ancora eliminati
da Q (che sono in Q o in Q verranno inseriti) diminuisce ad ogni esecuzione
del corpo del while (1) e può essere usato per dimostrare
la sua terminazione.