Elementi di Software Dependability -Interpretazione Astratta

Interpretazione astratta

Abstrazione: selezionare una proprietà

Abstrazione: selezionare una (delle) proprietà.

Abstrazione e correttezza

Astrare un insieme di punti nel piano.

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.

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 è un calcolo di punto fisso.
• Sarà inoltre possibile calcolare una approssimazione corretta della semantica 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 e ::= n | e*e³

• La semantica di questo linguaggio si può descrivere mediante una funzione definita da: η_Z: Exp → η = n η(n) * e = η(e)₁ η(e₂)

Semantica astratta

• Possiamo considerare un’astrazione della semantica concreta che calcola solo il segno delle espressioni Exp {-,0,+}.

σ: a - 0 +

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:

• η(e) < 0 ⇒ σ(e) = -
• η(e) = 0 ⇒ σ(e) = 0
• η(e) > 0 ⇒ σ(e) = +

Una prospettiva diversa

• Possiamo associare ad ogni valore astratto l’insieme di valori concreti che esso rappresenta: P(Z).

γ: {-,0,+} → Z

• γ(-) = {x ∈ Z | x < 0}
• γ(0) = {0}
• γ(+) = {x ∈ Z | x > 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 semantica concreta {η(e)} ⊆ γ(σ(e)).
• La funzione di concretizzazione stabilisce la relazione tra il concetto di approssimazione nei due domini concreto ed astratto.

Aggiungiamo -

• Aggiungiamo al nostro tiny language l’operatore unario di cambiamento di segno.

Exp e ::= n | e*e | -e³ = - η(e) η(-e) = - dove:

• - (-) = +,
• - (0) = 0,
• - (+) = -

σ(-e) = σ(e)

Aggiungiamo +

Aggiungere l’addizione è più complesso, in quanto il dominio astratto non è chiuso rispetto a questa operazione.