Astrazione e Concretizzazione
In una Interpretazione Astratta ci aspettiamo che il
seguente diagramma commuti (correttezza):

 (e )   ( (e ))
 (e )   ({  (e )})
Tino Cortesi
Exp
Tecniche di Analisi di Programmi
A

 
  2D
1
Correttezza
Per la correttezza dell’analisi sono sufficienti le
seguenti condizioni:
 e  formano una Galois insertion
id    , id   
 e  sono monotone
x  y   (x )   ( y )
Le operazioni astratte op sono corrette localmente :
 (op(s1 ,..., sn ))  op( (s1 ), ...,  (sn ))
Tino Cortesi
Tecniche di Analisi di Programmi
2
Correttezza locale
La condizione di correttezza locale garantisce che il risultato
dell’applicazione dell’operazione agli elementi astratti si sia una
corretta approssimazione di tutte le operazioni concrete (sugli
elementi rappresentati dagli si ).
 (op(s1 ,..., sn ))  op( (s1 ),...,  (sn ))
Per ogni operazione concreta, una operazione astratta corretta
c’e’ sempre (quella che restituisce sempre l’elemento massimo
del dominio astratto)
Tino Cortesi
Tecniche di Analisi di Programmi
3
Correttezza locale
A
op
A


D
2
 (op(s1 ,..., sn ))
op
D
2
op( (s1 ),...,  (sn ))
Tino Cortesi
Tecniche di Analisi di Programmi
4
Inserzione di Galois
x  2D . x   ( (x ))
a  A. x   ( (x ))
{-1,0,1}
T
{-1,0}
{-1,1}
{0,1}
{-1}
{0}
{1}

0



Tino Cortesi
Tecniche di Analisi di Programmi
5
Prova di correttezza
Proviamo per induzione sulla struttura di e che
 (e )   ( (e ))
Passo base:
 (i )

i
def. di 
 {i }
  ( ({i }))
  ( (i))
Tino Cortesi
inserzione di Galois
def di 
Tecniche di Analisi di Programmi
6
Prova di correttezza
Proviamo per induzione sulla struttura di e che
Step
 (e )   ( (e ))
 (e1 op e2 )
  (e1 ) op  (e2 )
def. di 
  ( (e1 )) op  ( (e2 )) per ipotesi induttiva
  ( (e1 ) op  (e2 ))

Tino Cortesi
 ( (e1 op e2 ))
correttezza locale
def di 
Tecniche di Analisi di Programmi
7
Correttezza
Possiamo definire la correttezza utilizzando
l’astrazione al posto della concretizzazione:
 (e )   ( (e ))   ({  (e )})   (e )
direzione 
 (e )   ( (e ))
{  (e )}   ( (e ))
 ({  (e )})   ( ( (e ))) monotonia
 ({  (e )})   (e )
   id
Tino Cortesi
Tecniche di Analisi di Programmi
8
Correttezza
L’altra direzione
 (e )   ( (e ))   ({  (e )})   (e )
direzione 
 ({  (e )})   (e )
 ( ({  (e )}))   ( (e )) monotonia
{  (e )}   ( (e ))
id   
 (e )   ( (e ))
Tino Cortesi
Tecniche di Analisi di Programmi
9
Aggiungere input
Il prossimo passo consiste nell’estendere il nostro
“tiny language” aggiungendo input.
Questo può essere modellato con la presenza di
variabili libere nelle espressioni
e  i | e  e | e | ... | x
Tino Cortesi
Tecniche di Analisi di Programmi
10
Semantica concreta
La firma della funzione semantica  diventa quindi
 : Exp  Int  Int
Un modo per scrivere questa funzione è pensarla come un
insieme di funzioni da Int a Int indicizzate con espressioni
i ( j )
x ( j )
e e ( j )
e e ( j )
Tino Cortesi
1
2
1
2
...


i
j
 e1 ( j ) e2 ( j )
 e1 ( j )  e2 ( j )

...
Tecniche di Analisi di Programmi
11
Semantica Astratta
La semantica astratta è data dalla funzione 
 : Exp  A  A
Come per la semantica concreta, possiamo indicizzare 
i ( j )
 i
x (j )
 j
 e e ( j )   e ( j )   e ( j )
1
2
1
2
 e e ( j )   e ( j )   e ( j )
...
i
Tino Cortesi
1
2
 ...
1
2
  ({i })
Tecniche di Analisi di Programmi
12
Correttezza
Bisogna generalizzare le condizioni di correttezza
Le seguenti condizioni sono equivalenti
i . e (i )   ( e ( ({i })))
e D   e 
A

 e A  e 
2
D
Tino Cortesi
Tecniche di Analisi di Programmi
e
A

 
e  2D
13
Correttezza locale
La correttezza locale la possiamo esprimere mediante
la seguenta regola:



op  ( e1 ( j )),...,  ( en ( j ))   op ( e1 ( j ),...,  en ( j ))
Tino Cortesi
Tecniche di Analisi di Programmi
14

La correttezza locale è sufficiente
Teorema: e ( j )   ( e ( j ))
Dimostrazione (per induzione)
Base
i ( j )  i   (i )   ( i ( j ))
x ( j )  j   ( j )   ( x ( j ))
Step
op (e ,...,e ) ( j )
 op ( e ( j ),..., e ( j ))
n
1
n
1
def. di 
 op ( ( e1 ( j )),...,  ( en ( j )) induzione
  (op ( e1 ( j ),...,  en ( j )))

Tino Cortesi
 ( op (e ,...,e ) ( j ))
1
n
correttezza locale
def. di 
Tecniche di Analisi di Programmi
15
Comando condizionale
e  ... | if e  e then e else e | ...
semantica concreta
 e3 (i ) if e1 (i )  e2 (i )
if e1 e2 then e3 else e4 (i )  
 e4 (i ) if e1 (i )  e2 (i )
semantica astratta
 if e e
1
2
then e3 else e4
(i )   e3 (i )



 e (i )
4
Si osservi l’utilizzo del least upper bound nel dominio astratto
Tino Cortesi
Tecniche di Analisi di Programmi
16
Comando condizionale :
correttezza
Assumiamo che sia vero il primo ramo del comando condizionale
(l’altro caso si dimostra allo stesso modo).
e (i )
3
  ( e3 (i ))
  ( e3 (i ))

   e3 (i )

 ( if e e
1
Tino Cortesi
2
per induzione
 ( e (i ))
4
 e (i ) 
monotonia di 
4
then e3 else e4
(i ))
Tecniche di Analisi di Programmi
17
Ricorsione
Aggiungiamo funzioni ricorsive (in una sola variabile,
per semplicità). Le funzioni possono essere dichiarate
e chiamate
program 
def f (x )  e
e  ... | f (e )
La funzione semantica che abbiamo considerato
finora è del tipo
 : Exp  Int  Int
Tino Cortesi
Tecniche di Analisi di Programmi
18
Semantica concreta rivista
Generalizziamo la funzione , per tener conto delle
chiamate di funzione.
  : Exp  (Int  Int )  Int  Int
f (e ) ( g )( j )  g ( e ( g )( j ))
x ( g )( j )
j
e e ( g )( j )  e ( g )( j )  e ( g )( j )
1
Tino Cortesi
2
1
Tecniche di Analisi di Programmi
2
19
Semantica delle funzioni ricorsive
  : Exp  (Int  Int )  Int  Int
Consideriamo una funzione
def f  e
Definiamo una catena ascendente f0 ,f1 ,... in Int  Int
f0  x . 
fi 1  e (fi )
Definiamo f 
Tino Cortesi
i
fi
Tecniche di Analisi di Programmi
20
Semantica delle funzioni ricorsive
def f = if x=0 then 1 else f(x - 1)
f0(i) = 
per ogni i
f1(i) = ’if x=0 then 1 else f(x - 1)(f0)(i) =
’1(f0)(i)
se
i=0
1
’f(x - 1)(f0)(i)
altrimenti
= f0 (’x - 1(f0)(i))
= f0 (’x (f0)(i)) - f0 (’1 (f0)(i))
= f0 (i) - f0 (1)
=
=
=
Tino Cortesi
Tecniche di Analisi di Programmi
21
def f = if x=0 then 1 else f(x - 1)
f0(i) =  per ogni i
f1(i) = 1 se i=0,  altrimenti
f2(i) = ’if x=0 then 1 else f(x - 1)(f1)(i) =
’1(f1)(i)
se
i=0
1
’f(x - 1)(f1)(i)
altrimenti
= f1 (’x - 1(f1)(i))
= f1 (’0 (f1)(i))
se x=1 [’0 (f1)(i)=0]
= f1(0) = 1
= f1 (j) (j#0)
altrimenti
=
=
=
Tino Cortesi
Tecniche di Analisi di Programmi
22
def f = if x=0 then 1 else f(x - 1)
f0(i)
f1(i)
f2(i)
f3(i)
f4(i)
...
=
=
=
=
=
(f) =
Tino Cortesi

1
1
1
1
per ogni i
se
i=0,  altrimenti
se
i=0,1,  altrimenti
se
i=0,1,2,  altrimenti
se
i=0,1,2,3,  altrimenti
Ui>=0 fi
Tecniche di Analisi di Programmi
23
Semantica astratta
In modo analogo, dobbiamo estendere la definizione della
semantica astratta .
Richiediamo che tutte le funzioni siano monotone.
  : Exp  (A  A)  A  A
 f (e ) ( g )(i )  g ( e ( g )(i ))
 x ( g )(i )
i
 e e ( g )(i )   e ( g )(i )   e ( g )(i )
1
Tino Cortesi
2
1
Tecniche di Analisi di Programmi
2
24
Semantica della ricorsione
 ': Exp  (A  A)  A  A
Consideriamo una funzione
def f  e
Definiamo una catena ascendente f 0 ,f 1 ,... in A  A
f 0  a . 
f i 1   e (f i )
Definiamo  f 
Tino Cortesi
fi
i
Tecniche di Analisi di Programmi
25
Correttezza
f2 ( j )

f1 ( j )

f0 ( j )



f2 ( j )

f 1(j )

f 0(j )
Elementi corrispondenti nelle due catene sono nella relazione
giusta
Tino Cortesi
Tecniche di Analisi di Programmi
26
Correttezza (continua)
i . fi ( j )   (f i ( j ))

i 0
fi ( j ) 
 (f i ( j ))
le catene convergono
i 0



fi ( j )    f i ( j )  monotonia di 
i 0
 i 0

 f ( j )   ( f ( j ))
per definizione
Tino Cortesi
Tecniche di Analisi di Programmi
27
Esempio
Consideriamo una funzione ricorsiva
def f(x) 
if x  0 then 1 else x  f(x  -1)
Astrazione
lfp   if x  0 then 1 else x  f(x  -1)  
Semplificando


lfp  f. x.   x  f(x  )
Tino Cortesi
Tecniche di Analisi di Programmi

28


lfp  f. x.   x  f(x  )

f 0  a . 
T
f i 1   e (f i )
f0

  0  T

    
f1 
0


  0  T
   

  0  T
f2 
 T T  T
f3 
Tino Cortesi


0
 T
 T T T T
Tecniche di Analisi di Programmi
29
Esempio (ctd)
Osserviamo che in questo caso l’astrazione non porta a nessuna
informazione utile
Le catene ascendenti sono strettamente crescente, fino a che
non convergono
f0  f1  f2  f3  f4  f5  ...
Ma non è detto che considerando un un singolo valore la catena
ascendente concreta sia strettamente crescente
f0 ()  f1 ()  f2 ()  f3 ()  f4 ()  f5 ()  ...
Tino Cortesi
Tecniche di Analisi di Programmi
30
Riassumendo…
Applicare le tecniche di Interpretazione
astratta significa
Definire semantica concreta ed astratta del
programma: domini ed operazioni
Applicare un algoritmo di punto fisso
Tino Cortesi
Tecniche di Analisi di Programmi
31
Conclusioni
Il lavoro in Cousot&Cousot ‘77 ha generato
un’enorme quantità di lavori scientifici
Uno slogan riassuntivo:
Analisi Statica = Reticoli + Funzioni monotone
E’ una teoria unificante. Ad es. le tecniche dataflow e
di model checking si possono esprimere in termini di
Interpretazione Astratta.
Tino Cortesi
Tecniche di Analisi di Programmi
32