Ricorsione
Aggiungiamo funzioni ricorsive (in una sola variabile,
per semplicità).
program 
def f (x )  e
e  ... | f (e )
La funzione semantica associata è del tipo
 : Exp  Int  Int
Tino Cortesi
Tecniche di Analisi di Programmi
1
Semantica concreta rivista
Generalizziamo la funzione m, 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
2
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
3
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
4
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 i=1 [’0 (f1)(1)=0]
= f1(0) = 1
= f1 (j) (j#0)
altrimenti
=
=
=
Tino Cortesi
Tecniche di Analisi di Programmi
5
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
6
Semantica astratta
In modo analogo, dobbiamo estendere la definizione della
semantica astratta s.
Richiediamo che tutte le funzioni siano monotone.
s  : Exp  (A  A)  A  A
s f (e ) ( g )(i )  g (s e ( g )(i ))
s x ( g )(i )
i
s e e ( g )(i )  s e ( g )(i )  s e ( g )(i )
1
Tino Cortesi
2
1
Tecniche di Analisi di Programmi
2
7
Semantica della ricorsione
s ': 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  s e (f i )
Definiamo s f 
Tino Cortesi
fi
i
Tecniche di Analisi di Programmi
8
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
9
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 )   (s f ( j ))
per definizione
Tino Cortesi
Tecniche di Analisi di Programmi
10
Semantica astratta
def f = if x=0 then 1 else f(x - 1)
f’0(i’) = 
per ogni i’ in {0,+,-,…}
f’1(i’) = s’if x=0 then 1 else f(x - 1)(f’0)(i’) =
s’1(f’0)(i)
=
lub
=+
f’2(i)= f’1(i)
Tino Cortesi
=
+
s’f(x - 1)(f’0)(i’)
= f’0 (s’x - 1(f’0)(i’))
= f0 (s’x (f’0)(i’)) - f0 (s’1 (f’0)(i’))
= f0 (i’) - f’0 (+)
=-=
Tecniche di Analisi di Programmi
11
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
12
Concrete
Semantics
Tuners
Abstract
Domain
Abstract
Domain
Tino Cortesi
Collecting
Semantics
Partitioning
Abstract
Semantics
Tecniche di Analisi di Programmi
Iterative
Resolution
Algorithms
13
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
14