Interpretazione Astratta
Astrazione:
selezionare una proprieta’
Tino Cortesi
Analisi e Verifica di Programmi
2
Astrazione:
selezionare una (delle) proprieta’
Tino Cortesi
Analisi e Verifica di Programmi
3
Astrazione e correttezza
Tino Cortesi
Analisi e Verifica di Programmi
4
Astrarre un insiemi di punti nel
piano…
Tino Cortesi
Analisi e Verifica di Programmi
5
Interpretazione Astratta
Una tecnica utilizzata da quasi 30 anni (Patrick e Radhia Cousot,
1977) per trattare in modo sistematico astrazioni e
approssimazioni
Nata per descrivere analisi statiche di programmi imperativi e
provarne la correttezza.
Sviluppata soprattutto su linguaggi dichiarativi (logici e
funzionali)
Vista oggi come tecnica generale per ragionare su semantiche a
diversi livelli di astrazione
Applicata con successo a sistemi distribuiti per verifica di
programmi (correttezza – sicurezza)
Tino Cortesi
Analisi e Verifica di Programmi
6
L’idea generale
il punto di partenza è la semantica concreta, ovvero una
funzione che assegna significati ai comandi di un programma in
un dominio fissato di computazione.
un dominio astratto, che modella alcune proprietà delle
computazione concrete, tralasciando la rimanente informazione
(dominio di computazione astratto)
derivare una semantica astratta, che permetta di eseguire il
programma sul dominio astratto per calcolare la proprietà che il
dominio astratto modella.
applicando un algoritmo di punto fisso sarà quindi possibile
calcolare staticamente una approssimazione corretta della
semantica astratta
Tino Cortesi
Analisi e Verifica di Programmi
7
Semantica concreta
Consideriamo un linguaggio molto limitato, che permette
unicamente di operare su moltiplicazioni di interi.
La semantica di questo linguaggio si può descrivere mediante
una funzione m definita da:
e  i |e e
m : Exp  Int
m (i )

i
m (e1  e2 )  m (e1 ) m (e2 )
Tino Cortesi
Analisi e Verifica di Programmi
8
Semantica astratta
Possiamo considerare un’astrazione della semantica concreta
(semantica astratta) che calcola solo il segno delle espressioni
 :Exp  ,-,0
  if i

 (i )
  0 if i
  if i

 (e1  e2 )   (e1 ) 
Tino Cortesi
 0

 0
 0 
 (e2 )
Analisi e Verifica di Programmi


0



0

0
0
0
0


0

9
Correttezza
Possiamo dimostrare che questa astrazione è corretta, ovvero
che predice correttamente il segno delle espressioni.
La dimostrazione è per induzione strutturale sull’espressione e,
ed utilizza le proprietà della moltiplicazione tra interi (il prodotto
di due positivi è positivo, ecc.).
m (e )  0   (e )  
m (e )  0   (e )  0
m (e )  0   (e )  
Tino Cortesi
Analisi e Verifica di Programmi
10
Una prospettiva diversa
Possiamo associare ad ogni valore astratto l’insieme di valori
concreti che esso rappresenta:
 : { , 0, }  2Int
Tino Cortesi
 ( ) 
 (0) 
i | i
 0
0
 ( ) 
i | i
 0
Analisi e Verifica di Programmi
11
Concretizzazione
La funzione di concretizzazione  mappa un valore astratto in un
insieme di valori concreti
Indichiamo con D il dominio concreto e con A il dominio astratto

m (e )   ( (e ))
Tino Cortesi
Exp
Analisi e Verifica di Programmi
m
A

2
D
12
Interpretazione Astratta
Questa è una Interpretazione Astratta.
Una computazione in un dominio astratto
In questo caso, il dominio è {+,0,-}.
La semantica astratta è corretta
è un’approssimazione della semantica concreta
La funzione di concretizzazione stabilisce la
connessione tra i due domini
Tino Cortesi
Analisi e Verifica di Programmi
13
Aggiungiamo Aggiungiamo al nostro tiny language l’operatore unario di
cambiamento di segno
m ( e )   m (e )
 ( e )   (e )
Tino Cortesi
Analisi e Verifica di Programmi


0


0

14
Aggiungiamo +
Aggiungere l’addizione è più complesso, in quanto il dominio
astratto non è chiuso rispetto a questa operazione


0

m (e1  e2 )

m (e1 )  m (e2 )



?
 (e1  e2 )

 (e1 )   (e2 )
0

0


?


A quale valore astratto corrisponde il risultato della somma di
due numeri interi con segno opposto?
Tino Cortesi
Analisi e Verifica di Programmi
15
Soluzione
Aggiungiamo un nuovo elemento astratto che rappresenta un
qualsiasi numero intero
 (T)  Int
Tino Cortesi
  0  T
   T T
0  0  T
 T   T
T T T T T
Analisi e Verifica di Programmi
16
Estendere le altre operazioni
Avendo aggiunto un elemento al dominio astratto, è necessario
estendere le operazioni astratte già definite
 
 
0 0
 
T T
Tino Cortesi
0  T
0  T
0 0 0
0  T
0 T T
  0  T
 0  T
Analisi e Verifica di Programmi
17
Esempi
In alcuni casi c’è perdita di informazione dovuta alle operazioni
m ((1  2)  3)

0
 ((1  2)  3)

(   )  ( )  T
In altri casi non c’è perdita di informazione
Tino Cortesi
m ((5  5)  6)

31
 ((5  5)  6)

(   )    
Analisi e Verifica di Programmi
18
Aggiungiamo /
Aggiungere la divisione intera (con resto) / non da problemi,
eccetto il caso della divisione per 0.
Se dividiamo gli intero di un insieme di interi per 0 che risultato
otteniamo? L’insieme vuoto.
Questo è rappresentato da un nuovo elemento, ^, rispetto al
quale si devono estendere le altre operazioni
( ^ )  
/

0
 T ^


0
 T ^
0
^ ^ ^ ^ ^


T T
0
 T ^
0 T T
^
^ ^ ^ ^ ^ ^
Tino Cortesi
Analisi e Verifica di Programmi
x

^
 ^

^

^
^ 
x
 ^
19
Il dominio astratto
Il dominio astratto è un reticolo
completo
L’ordine parziale è coerente con la
funzione di concretizzazione:
x  y   (x )   (y )
Ogni sottoinsieme ha un least upper
bound (lub) ed un greatest lower
bound (glb): è un reticolo completo
Tino Cortesi
Analisi e Verifica di Programmi
T

0

^
20
La funzione di astrazione
Alla funzione di concretizzazione  corrisponde una funzione di
astrazione a.
La funzione a mappa insiemi di valori concreti in un valore
astratto (il più piccolo che li rappresenta tutti).
Nel nostro esempio,
a : 2Int  A
a (S )  lub  | i  0  i  S , 0 | 0  S ,  | i  0  i  S 
 (i )  a ({i })
Tino Cortesi
Analisi e Verifica di Programmi
21
Definizione Generale
Una Interpretazione Astratta consiste in:
Un dominio astratto A ed un dominio concreto D
A e D reticoli completi. L’ordine riflette la precisione (più
piccolo = più preciso)
Funzioni di concretizzazione e di astrazione monotone, che
formino una inserzione di Galois.
Una funzione che astrae correttamente la semantica
(operazioni astratte).
Inserzione di Galois:
x  2D . x   (a (x ))
a  A. x  a ( (x ))
Tino Cortesi
Analisi e Verifica di Programmi
22
sign (x)
, if x= bot
{y|y>0}, if x= +
{y|y0}, if x= 0+
{0}, if x= 0
{y|y0}, if x= 0{y|y<0}, if x= Z, if x= top
Un altro esempio
top
0-
0+
0
+
bot
asign y) = glb di
bot , if y= 
- , if y  {z| z < 0}
0- , if y  {z | z  0}
0 , if y  {0}
0+ , if y  {z | z  0}
+ , if y  {z | z  0}
top , if y  Z
Tino Cortesi
asign({0,1,3})= 0+
sign(0+)  {0,1,3}, {3,34,2}, ...
sign(asign({0,1,3}))  {0,1,3}
asign(sign(0+)) = 0+
Analisi e Verifica di Programmi
23
Inserzioni di Galois
(C, ), (A, )
: A  C (concretizzazione)
a: C  A (astrazione)

C
a ,  monotone
xC. x  ax
yA. ay  y
a ,  si determinano a vicenda
Tino Cortesi
Analisi e Verifica di Programmi
A
a
24
Operazioni astratte
Astrarre una funzione in modo ottimale: f# =   f  a
f#
Abstract domain

a
f
Concrete domain
Tino Cortesi
Analisi e Verifica di Programmi
25
Astrazioni come chiusure
Il dominio astratto può essere ottenuto dividendo il dominio
concreto in sottoinsiemi (non disgiunti) ai.
La funzione di astrazione mappa un sottoinsieme del dominio
nel più piccolo di questi ai che lo contiene.
Tino Cortesi
Analisi e Verifica di Programmi
26