Astrazione e Concretizzazione
In una Interpretazione Astratta ci aspettiamo che il
seguente diagramma commuti:

 (e )   ( (e ))
 (e )   ({  (e )})
Tino Cortesi
Exp
Tecniche di Analisi di Programmi
A

 
  2D
1
Correttezza
Per la correttezza dell’analisi sono necessarie 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
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
5
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
6
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
7
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
8
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
9
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
10
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
11
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
12
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
13

Prova di correttezza
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
14
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
15
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
16