Elementi di Software Dependability -Interpretazione Astratta

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

Altro esempio

(x) =

γ sign , se x =

; ?

• >

{y2Z|y>0}, se x = +

• {y2Z|y≥0}, se x = 0+ 0- 0+

• {0}, se x = 0

• 0

{y2Z|y≤0}, se x = 0- - +

• {y2Z|y<0}, se x = -

• se x =

Z, >

• ?

= glb di

α (S)

sign se S = ({0,1,3})= 0+

α

?, ∅

• sign

-, se S {z2Z|z < 0} (0+) ⊇ {0,1,3}, {3,5,2}, ...

⊆

• γ sign

0-, se S {z2Z|z 0}

≤

⊆

• 0, se S {0} ( ({0,1,3})) ⊇ {0,1,3}

γ α

=

• sign sign

0+, se S {z2Z|z 0}

≥

⊆

• ( (0+)) = 0+

α γ

sign sign

+, se S {z2Z|z 0}

>

⊆

• se S Z

>, µ

• 23

Connessione di Galois

(α, C, A, GC (Galois connection) se

γ)

1) A e C poset

2) A monotona (funzione di astrazione)

!

α:C

3) : A C monotona (funzione di concretizzazione)

!

γ

4) c

8c2C. · γ(α(c))

C

5) a

8a2A. ·

α(γ(a)) A 24

Inserzione di Galois

(α, C, A, GC e` una Galois insertion (GI) se

γ)

vale una delle seguenti condizioni equivalenti:

1) suriettiva

α

2) iniettiva

γ

3) = a

8a2A. α(γ(a)) 25

Aggiunzioni

(α, C, A, aggiunzione se

γ)

1) A e C poset

2) A (astrazione)

!

α:C

3) : A C (concretizzazione)

!

γ

4) a c

8c2C. 8a2A. · , ·

α(c) γ(a)

A C

FATTO: (α,C,A,γ) GC (α,C,A,γ) aggiunzione

, 26

Galois Insertion: proprieta`

(α, C, A, GI tra reticoli completi

γ)

(1) = | c

Æ{a2A ·

α(c) γ(a)}

C

(2) = | a}

Ç{c2C ·

γ(a) α(c) A

(3) QUINDI: determina e viceversa

α γ

(4) preserva i lub’s

α

(5) preserva i glb’s

γ

(6) ) = e ) =

? >

α(? γ(>

C A A C

(7) se una funzione tra reticoli completi preserva i lub’s allora

C A

α : !

posso definire la come in (2) che forma con una GI

γ α

(8) se una funzione preserva i glb’s allora posso definire la

A C

γ : α

!

come in (1) che forma con una GI

γ 27

Galois Insertion: proprieta`

Come "trasformare" una GC (α, C, A, in una GI eliminando i valori

γ)

astratti "inutili"?

Semplicemente considero come dominio astratto "ridotto" (reduced)

A = e considero le restrizioni delle medesime funzioni di

red α(C)

astrazione e concretizzazione:

: C A dove (c) =

red red red

!

α α α(c)

: A C dove (a) =

red red red

!

γ γ γ(a)

Banalmente, (α , C, A , ) e' diventata una GI con lo stesso

red red red

γ

"potere espressivo" della GC di partenza. 28

Astrazioni come chiusure

• Il dominio astratto specificato come una GI (α,C,A,γ)

induce una partizione del dominio concreto:

c c ) = )

» , α(c α(c

1 2 1 2

• Per ogni classe di equivalenza [c] esiste il lub, cioe’

»

ogni classe di equivalenza ha un rappresentante

canonico

• La funzione C che mappa un valore concreto c

ρ:C!

a questo rappresentante [c] e` un operatore di

Ç c »

chiusura su C 29

Chiusure

• Un operatore : C C su un poset C e`

!

ρ

una chiusura se:

– e` monotona

ρ

– e` crescente: x ·

ρ ρ(x)

– e` idempotente: =

ρ ρ(ρ(x)) ρ(x)

• uco(C) denota l'insieme di tutte le chiusure

su C 30

Chiusure e GI

• Una GI (α,C,A,γ) induce una chiusura :C!C

ρ

A

definita come: [c]

,

(c) = {x2C | =

Ç Ç

ρ γ±α(c) α(x)·α(c)} c

A C »

• Una chiusura C su un reticolo completo C

!

ρ:C

induce una GI (ρ,C,img (C),id)

ρ

• Queste due trasformazioni sono una l’inversa

dell’altra

• QUINDI: la specifica di un dominio astratto puo`

essere data equivalentemente tramite una GI o una

chiusura 31

Proprieta` delle Chiusure

1. Una chiusura uco(C) (con C reticolo completo) e` univocamente

2

ρ

determinata dalla sua immagine

,

img (C) {ρ(x) | x2C}

ρ

= (C) | x y}

Æ{y2img ·

2. ρ(x) ρ

,

3. img (C) = fix(ρ) {x2C | ρ(x)=x}

ρ

4. XµC e` l’immagine di una chiusura su C iff X e` una Moore-family

ρ

X

di C, cioe` X=M(X), {ÆS | Sµ X} (dove =

> Æ? 2 M(X))

,

5. Quindi, se X e` una Moore-family allora X | x y} e` la

2 ·

ρ λx.Æ{y

X

corrispondente chiusura

6. e` detta la chiusura di Moore (Moore-closure) di X in C, cioe`

M(X) e` il piu` piccolo sottoinsieme di C che contiene X ed e` una

M(X)

Moore-family

7. VALE: = e img(ρ )=X

ρ ρ

img X

ρ

8. QUINDI: chiusure su C sono in biezione con Moore-families di C 32

Proprieta` delle Chiusure

Teorema: Se C e` un reticolo completo allora uco(C) e` un

reticolo completo (uco(C),v,t,u,λx.> , dove:

λx.x)

C

– iff C. iff img(ρ) img(µ)

v 8y2 · µ

µ ρ µ(y) ρ(y)

C

– = (x) e img(u ) = img(ρ ))

u M([

ρ λx.Æ ρ ρ

i2 I i i2 I i i2 I i i2 I i

– img(t ) = img(ρ )

Å

ρ

i2 I i i2 I i

– e` la chiusura top mentre e` la chiusura bottom

λx.> λx.x

C 33

Il Reticolo dei Domini Astratti

• uco(C) viene detto il reticolo dei domini astratti

• se A e A sono due astrazioni di un dominio concreto

1 2

comune C, specificate mediante GI, allora A e` piu` preciso

1

(o piu` concreto, o meno approssimato) di A , denotato da

2

A A , quando (come chiusure)

v v

ρ ρ

1 2 A1 A2

• A e A si dicono astrazioni equivalenti quando =ρ

ρ

1 2 A1 A2

• Lub’s and glb’s in uco(C) si possono quindi interpretare nel

seguente modo: sia {A } una famiglia qualsiasi di astrazioni

i i2 I

di C

– A e` il piu` concreto tra i domini che sono astrazioni di tutti

t i2 I i

gli A i

– A e` il piu` astratto tra tutti i domini che sono piu` precisi di

u i2 I i

tutti gli A

i 34

Astrazione e Concretizzazione

• In una interpretazione astratta ci aspettiamo

che il seguente diagramma commuti: A

σ ·

µ

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

Exp µ

·

α({η(e)}) σ(e) η Z {·} P(Z) 35

Correttezza

• Per la correttezza dell’analisi sono necessarie le

seguenti condizioni

• (α,C,A,γ) e` una GI

• Le operazioni astratte op (che sono supposte essere

a

monotone) sono corrette rispetto alle corrispondenti

operazioni concrete op (che sono pure supposte

essere monotone): per ogni ,...,a A

n

ha i 2

1 n

op(γ(a ),...,γ(a )) (a ,...,a ))

a

· γ(op

1 n C 1 n

• La correttezza di un'operazione astratta op puo`

a

essere equivalentemente definita come: per ogni

,...,c C n

hc i 2

1 n

,...,c )) op (α(c ),...,α(c ))

a

·

α(op(c 1 n A 1 n 36