Elementi di Software Dependability -Interpretazione Astratta

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 ::= n | e*e

La semantica di questo linguaggio si può descrivere mediante una funzione definita da:

ηZ: Exp !η = n

η(n) *e ) = )£η(e )η(e η(e1 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 σ(e1 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 espressione e ∈ Exp: < 0 = -, η(e) σ(e) = 0 = 0, η(e) σ(e) > 0 = +, η(e) σ(e) Una prospettiva diversa • Possiamo associare ad ogni valore astratto l'insieme di valori concreti che esso rappresenta: P(Z) γ: {-,0,+} Z = {x² | x < 0} γ(-) = {0} γ(0) Z = {x² | x > 0} γ(+) = {0} 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)² γ(σ(e)) η D {•} P(D) 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 semanticaconcretaη(e) µ γ(σ(e))• La funzione di concretizzazione stabilisce la relazione tra il concetto di approssimazione nei due domini concreto ed astratto 13Aggiungiamo -• Aggiungiamo al nostro tiny language l'operatore unario di cambiamento di segnoExp e ::= n | e*e | -e3= -η(e)η(-e) = - dove - (-) = +, - (0) = 0, - (+) = -a a a aσ(-e) σ(e) 14Aggiungiamo +• Aggiungere l'addizione è più complesso, in quanto il dominio astratto non è chiuso rispetto a questa operazione+a - 0 ++ e ) = ) + )η(e η(e η(e1 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? 15Soluzione• Aggiungiamo un nuovo valore astratto che rappresenta un qualsiasi numero intero+a - 0 + >- - - > >Z=γ(>) 0 - 0 + >+ + +> >> > > > > 16Estendere le

altre operazioni• Avendo aggiunto un elemento al dominio astratto, ènecessario estendere le operazioni astratte giàdefinitea - 0 + - (-) = +, - (0) = 0,a a£ > - (+) = -, - (>) =a a >- + 0 - >0 0 0 0 0+ - 0 + >0> > > > 17

EsempiIn 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 delladivisione per 0• Se dividiamo un insieme di interi per 0 che risultato otteniamo?L’insieme vuoto. Quindi la semantica concreta assumera` i propri valoriZ,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 = = xa a0 ? £ ? £ ?? ⊥ ⊥ ⊥ ⊥ - (?) =a ?+ - 0 + > ⊥0> > > > ⊥⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 19Il dominio astratto• Il dominio astratto è un poset incui 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 edun glb: è quindi un reticolocompleto 20La 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;, µ≠ <0A = 0 se S = {0}!α:P(Z) α(S) Z+ se S S;,

µ≠ >0altrimenti> 21Definizione 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, cheformano una inserzione di Galois.– Operazioni astratte che astraggono correttamente su A lasemantica concreta su C.

• Inserzione di Galois: funzioni monotone e taliα:C!A γ:A!Cche: C. c8c 2 · γ(α(c))CA. a =8a 2 α(γ(a)) 22Altro 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}, ...⊆• γ sign0-

GC e` una Galois insertion (GI) seγ)vale una delle seguenti condizioni equivalenti: 1) suriettivaα 2) iniettivaγ 3) = a8a2A. α(γ(a)) 25Aggiunzioni(α, C, A, aggiunzione seγ)1) A e C poset 2) A (astrazione)!α:C 3) : A C (concretizzazione)!γ 4) a c8c2C. 8a2A. · , ·α(c) γ(a) CFATTO: (α,C,A,γ) GC (α,C,A,γ) aggiunzione, 26Galois Insertion: proprieta`(α, C, A, GC e` una Galois insertion (GI) seγ)vale una delle seguenti condizioni equivalenti: 1) suriettivaα 2) iniettivaγ 3) = a8a2A. α(γ(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 alloraC Aα : !posso definire la come in (2) che forma con una GIγ α(8) se una funzione preserva i glb’s allora posso definire laA Cγ : α!come in (1) che forma con una GIγ 27Galois 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 dired α(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 γ"potere espressivo" della GC di partenza. 28Astrazioni come chiusure• Il dominio astratto specificato come una GI (α,C,A,γ) induce una partizione del dominio concreto:c c ) = )» , α(c α(c1 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 29Chiusure• 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 chiusuresu C 30Chiusure e GI• Una GI (α,C,A,γ) induce una chiusura :C!CρAdefinita come: [c],(c) = {x2C | =Ç Çρ

γ±α(c) α(x)·α(c)} cA C »• Una chiusura C su un reticolo completo C!ρ:Cinduce una GI (ρ,C,img (C),id)ρ• Queste due trasformazioni sono una l’inversadell&r ^{γ±α(c) α(x)·α(c)} cA C »• Una chiusura C su un reticolo completo C!ρ:Cinduce una GI (ρ,C,img (C),id)ρ• Queste due trasformazioni sono una l’inversadell&r}