Che materia stai cercando?

Elementi di Software Dependability -Interpretazione Astratta

Appunti di Elementi di Software Dependability -Interpretazione Astratta. Nello specifico gli argomenti trattati sono i seguenti: Il punto di partenza è la semantica concreta, Un dominio astratto, Derivare una semantica astratta, Semantica concreta, ecc.

Esame di Elementi di Software Dependability docente Prof. U. Monile

Anteprima

ESTRATTO DOCUMENTO

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


PAGINE

40

PESO

436.92 KB

AUTORE

Sara F

PUBBLICATO

+1 anno fa


DETTAGLI
Corso di laurea: Corso di laurea in ingegneria informatica
SSD:
Università: Firenze - Unifi
A.A.: 2013-2014

I contenuti di questa pagina costituiscono rielaborazioni personali del Publisher Sara F di informazioni apprese con la frequenza delle lezioni di Elementi di Software Dependability e studio autonomo di eventuali libri di riferimento in preparazione dell'esame finale o della tesi. Non devono intendersi come materiale ufficiale dell'università Firenze - Unifi o del prof Monile Umberto.

Acquista con carta o conto PayPal

Scarica il file tutte le volte che vuoi

Paga con un conto PayPal per usufruire della garanzia Soddisfatto o rimborsato

Recensioni
Ti è piaciuto questo appunto? Valutalo!

Altri appunti di Elementi di software dependability

Elementi di Software Dependability
Appunto
Elementi di Software Dependability -Interpretazione Astratta – Verifica codice
Dispensa
Elementi di Software Dependability - Software Safety
Appunto
Elementi di Software Dependability - Formal Methods in Practice
Dispensa