Elementi di Software Dependability -Interpretazione Astratta

Astrarre un insiemi di punti nel

piano 5

Interpretazione Astratta

• Una tecnica utilizzata da circa 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 per varie classi di linguaggi di

programmazione e sistemi reattivi

• Vista oggi come tecnica generale per ragionare su

semantiche a diversi livelli di astrazione 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

computazioni concrete, tralasciando la rimanente informazione

(dominio di computazione astratto).

• Derivare una semantica astratta, che permetta di “eseguire

astrattamente” il programma sul dominio astratto per calcolare

la proprietà che il dominio astratto modella.

• Il calcolo della semantica astratta tipicamente e` un calcolo di

punto fisso.

• Sarà inoltre possibile calcolare una approssimazione corretta

della semantica astratta. 7

Semantica concreta

• Considereremo un linguaggio pseudo-funzionale di

base piuttosto che un linguaggio imperativo nello stile

While

• Iniziamo da un linguaggio molto limitato, che

permette unicamente di moltiplicare interi.

Exp e ::= n | e*e

3

• La semantica di questo linguaggio si può descrivere

mediante una funzione definita da:

η

Z

: Exp !

η = n

η(n) *e ) = )£η(e )

η(e η(e

1 2 1 2 8

Semantica astratta

• Possiamo considerare un’astrazione della semantica

concreta (semantica astratta) che calcola solo il

segno delle espressioni

Exp {-,0,+}

!

σ: a - 0 +

£

- se n<0 - + 0 -

= 0 se n=0

σ(n) 0 0 0 0

+ se n>0 + - 0 +

*e ) = ) )

a

£

σ(e σ(e σ(e

1 2 1 2 9

Correttezza

• Possiamo dimostrare che questa astrazione è corretta, ovvero

che prevede correttamente il segno delle espressioni.

• La dimostrazione è per induzione strutturale sull’espressione e

semplicemente utilizza le proprietà della moltiplicazione tra interi

(il prodotto di due positivi è positivo, etc.).

Per ogni expressione e2Exp:

< 0 = -

,

η(e) σ(e)

= 0 = 0

,

η(e) σ(e)

> 0 = +

,

η(e) σ(e) 10

Una prospettiva diversa

• Possiamo associare ad ogni valore astratto l’insieme

di valori concreti che esso rappresenta:

! P(Z)

γ:{-,0,+} Z

= {x2 | x<0}

γ(-) = {0}

γ(0) Z

= {x2 | x>0}

γ(+) 11

Concretizzazione

• La funzione di concretizzazione mappa un valore

γ

astratto in un insieme di valori concreti

• Indichiamo con D il dominio concreto dei valori e con

A il dominio astratto A

σ γ

Exp

η(e)2γ(σ(e)) η D {·} P(D) 12

Interpretazione Astratta

• Abbiamo specificato una interpretazione astratta.

– Computazioni astratte in un dominio astratto

– In questo caso, il dominio astratto è {+,0,-}.

• La semantica astratta è corretta

– è un’approssimazione della semantica concreta

{η(e)} µ γ(σ(e))

• La funzione di concretizzazione stabilisce la relazione

tra il concetto di approssimazione nei due domini

concreto ed astratto 13

Aggiungiamo -

• Aggiungiamo al nostro tiny language l’operatore

unario di cambiamento di segno

Exp e ::= n | e*e | -e

3

= -η(e)

η(-e) = - dove - (-) = +, - (0) = 0, - (+) = -

a a a a

σ(-e) σ(e) 14

Aggiungiamo +

• Aggiungere l’addizione è più complesso, in quanto il dominio

astratto non è chiuso rispetto a questa operazione

+

a - 0 +

+ e ) = ) + )

η(e η(e η(e

1 2 1 2 - - - ?

+ e ) = ) + )

a

σ(e σ(e σ(e 0 - 0 +

1 2 1 2 + ? + +

• A quale valore astratto corrisponde il risultato della somma di

due numeri interi con segno opposto? 15

Soluzione

• Aggiungiamo un nuovo valore astratto che

>

rappresenta un qualsiasi numero intero

+

a - 0 + >

- - - > >

Z

=

γ(>) 0 - 0 + >

+ + +

> >

> > > > > 16

Estendere le altre operazioni

• Avendo aggiunto un elemento al dominio astratto, è

necessario estendere le operazioni astratte già

definite

a - 0 + - (-) = +, - (0) = 0,

a a

£ > - (+) = -, - (>) =

a a >

- + 0 - >

0 0 0 0 0

+ - 0 + >

0

> > > > 17

Esempi

In alcuni casi c’è perdita di informazione dovuta alle operazioni

• - 3) = 0

η((1+2) -3) = (+ + +) + - = + + - =

a a a >

σ((1+2)+

In altri casi non c’è perdita di informazione

• + 6) = 26

η((5*4) + 6) = (+ +) + + = + + + = +

a a a

£

σ((5*4) 18

Aggiungiamo la divisione

• Aggiungere la divisione intera / non crea problemi, eccetto il caso della

divisione per 0

• Se dividiamo un insieme di interi per 0 che risultato otteniamo?

L’insieme vuoto. Quindi la semantica concreta assumera` i propri valori

Z,

sul powerset di cioe` ! P(Z)

η:Exp

• L’insieme vuoto di interi è rappresentato da un nuovo elemento ⊥

astratto rispetto al quale si devono estendere le altre operazioni

/ - 0 +

a > ⊥ + x = = x +

a a

- + 0 - > ? ? ?

⊥

γ(?)=; x = = x

a a

0 ? £ ? £ ?

? ⊥ ⊥ ⊥ ⊥ - (?) =

a ?

+ - 0 + > ⊥

0

> > > > ⊥

⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 19

Il dominio astratto

• Il dominio astratto è un poset in

cui l’ordine parziale rappresenta >

la nozione di approssimazione/

precisione

• L’ordine parziale è coerente con 0

- +

la funzione di concretizzazione:

x y

· , µ

γ(x) γ(y) ?

• Ogni sottoinsieme ha un lub ed

un glb: è quindi un reticolo

completo 20

La funzione di astrazione

• Alla funzione di concretizzazione corrisponde una

γ

funzione di astrazione α.

• La funzione mappa un insieme S di valori concreti

α

nel piu` preciso valore astratto che rappresenta S.

• Nel nostro esempio se S =

? ; Z

- se S S

;, µ

≠ <0

A = 0 se S = {0}

!

α:P(Z) α(S) Z

+ se S S

;, µ

≠ >0

altrimenti

> 21

Definizione Generale

• Una Interpretazione Astratta consiste in:

– Un dominio astratto A ed un dominio concreto C

– A e C reticoli completi. L’ordine riflette la precisione/

approssimazione (più piccolo = più preciso)

– Funzioni di concretizzazione e di astrazione monotone, che

formano una inserzione di Galois.

– Operazioni astratte che astraggono correttamente su A la

semantica concreta su C.

• Inserzione di Galois: funzioni monotone e tali

α:C!A γ:A!C

che: C. c

8c 2 · γ(α(c))

C

A. a =

8a 2 α(γ(a)) 22