Simone Martini A.A. 1995/1996 Università di Udine September 17, 1996

Esercizi e complementi di Semantica Formale dei Liguaggi di Programmazione

per il corso di Metodi per il trattamento dell’informazione

Vengono descritte due diverse ed indipendenti estensioni del linguaggio IMP.

1 Blocco espressione

Sintassi: La categoria sintattica AExp è estesa con la clausola:

a ::= begin c val a end

1.1 Semantica operazionale

Possiamo dar semantica a begin c val a end in due modi diversi. Il primo, apparentemente più semplice è

\frac{< c, σ >→ σ′  < a, σ′ >→ n}{< begin c val a end, σ >→ n}  (1)

Si tratta di una semantica di difficile implementazione,.in quanto implica un salvataggio dello stato subito prima della valutazione di un blocco espressione, in modo da poterlo ripristinare al termine della valutazione stessa, come esemplificato dall’esempio seguente.

Sia σ = {x→1; y→0}. Con la clausola (1) si ha

< x := 1; y := begin x := x + 1 val x end, σ >→ {x→1; y→2}

Siccome i blocchi espressione possono essere arbitrariamente annidati l’uno nell’altro, il linguaggio risultante da questa semantica per il blocco espressione è multiple-threaded, nel senso che più flussi di controllo sono (potenzialmente) contemporaneamente attivi.

La semantica di più semplice realizzazione (nonché più ovvia per il programmatore) è quella in cui le modifiche allo stato effettuate all’interno del blocco espressione hanno effetti globali (questa è la semantica del blocco espressione in Algol e corrisponde anche a quella forma assai impura di blocco espressione che è il corpo di una funzione Pascal). Questa interpretazione, tuttavia, implica una modifica non da poco della semantica del linguaggio: adesso le espressioni (aritmetiche e, di riflesso, logiche) possono modificare lo stato per effetto collaterale.

La valutazione delle espressioni non è più una relazione tra AExp, Stati e AVal, ma assumerà la forma

< a, σ >→< n, σ′ >

con il significato intuitivo: “la valutazione di a nello stato σ produce il valore n, modificando lo stato in σ′”. La clausola per il blocco espressione potrà essere formulata come

\frac{< c, σ >→ σ′ < a, σ′ >→< n, σ′′ >}{< begin c val a end, σ >→< n, σ′′ >}

ma corrispondentemente si dovranno modificare le clausole delle altre espressioni e comandi. Diamo la sola clausola per le espressioni composte:

\frac{< a_{1}, σ >→< n_{1}, σ_{1} >  < a_{2}, σ_{1} >→< n_{2}, σ_{2} >  n = n_{1} op n_{2}}{< a_{1} op a_{2}, σ >→< n, σ_{2} >}

Esercizio: Si diano le clausole per le espressioni booleane e per i comandi.

1.2 Semantica denotazionale

Il tipo della funzione A è modificato in:

A : AExp → Store_{⊥} → Val × Store_{⊥}

Clausole principali^{1}:

A[[n]]  = \underline{λ}s.(n, s)
A[[X]]  = \underline{λ}s.(s(X), s)
A[[a_{1} op a_{2}]]  = \underline{λ}s.let (n_{1}, s_{1}) ⇐ A[[a_{1}]]s in
let (n_{2}, s_{2}) ⇐ A[[a_{2}]]s_{1} in (n_{1} op_{⊥}n_{2}, s_{2})
A[[begin c val a end]] = \underline{λ}s.let s′ ⇐ C[[c]] in A[[a]]s′

Si osservi come la clausola per le operazioni forzi un ordinamento di valutazione da sinistra a destra. Vengono corrispondentemente modificati tipi e clausole di B e C:

B : BExp → Store_{⊥} → Bool × Store_{⊥}
C : Com → Store_{⊥} → Store_{⊥}.

Alcune clausole per B:

B[[true]]  = \underline{λ}s.(true, s)
B[[false]]  = \underline{λ}s.(false, s)
B[[a_{1} = a_{2}]] = \underline{λ}s.let (n_{1}, s_{1}) ⇐ A[[a_{1}]]s in
let (n_{2}, s_{2}) ⇐ A[[a_{2}]]s_{1} in (n_{1} = n_{2}, s_{2})

e quelle per C:

C[[skip]]  = \underline{λ}s.s
C[[X := a]]  = \underline{λ}s.let (n_{1}, s_{1}) ⇐ A[[a]]s in s_{1}[n_{1}/X].
C[[if b then c_{1} else c_{2}]] = \underline{λ}s.let (t, s′) ⇐ B[[b]]s in COND(t, C[[c_{1}]]s′, C[[c_{2}]]s′)
C[[while b do c]]  = fix(λf.λs.let (t, s′) ⇐ B[[b]]s in COND(t, f(C[[c]]s′), s′)).

2 Non terminazione vs. errore di un’operazione

Domini Semantici

Val  = N + {err}
BVal  = B + {err}
Store  = [Loc → N]
ResStore = Store + Store

Assumiamo che Val, BVal e ResStore si ottengano rispettivamente mediante le iniezioni

N ⟶^{v} Val ⟵^{e} {err} B ⟶^{v} BVal ⟵^{e} {err} Store ⟶^{OK} ResStore ⟵^{ER} Store.

Funzioni Semantiche per le espressioni

A : AExp → Store → Val
B : BExp → Store → BVal

1Per semplificare la notazione si usa un “let” con pattern-matching. Formalmente: let (n_{1}, s_{1}) ⇐ A in E è un’abbreviazione per let a ⇐ A in let n_{1} ⇐ fst(a) in let s_{1} ⇐ snd(a) in E.

Clausole per espressioni aritmetiche

A[[n]]  = λs.v(n)
A[[X]]  = λs.v(s(X))
A[[a_{1} + a_{2}]] = λs.case A[[a_{1}]]s of

e(err).e(err) |

v(n_{1}).case A[[a_{2}]]s of

e(err).e(err) |
v(n_{2}).v(n_{1} + n_{2})

end end

A[[a_{1} ∗ a_{2}]] = analogo a +
A[[a_{1} − a_{2}]] = λs.case A[[a_{1}]]s of

e(err).e(err) |

v(n_{1}).case A[[a_{2}]]s of

e(err).e(err) |
COND(n_{1} ≥ n_{2}, v(n_{1} − n_{2}), e(err))

end end

Le clausole per B sono modificate analogamente, in modo da far propagare il valore di errore; per esempio:

B[[a_{1} = a_{2}]] = λs.case A[[a_{1}]]s of

e(err).e(err) |

v(n_{1}).case A[[a_{2}]]s of

e(err).e(err) |
v(n_{2}).v(n_{1} = n_{2})

end end

La funzione di interpretazione semantica per i comandi è più complessa. Per il suo tipo abbiamo a disposizioni varie opzioni. Quella più vicina alle clausole standard di IMP, e che adotteremo per le clausole che daremo, è

C : Com → ResStore_{⊥} → ResStore_{⊥}.

anche se C : Com → Store → ResStore_{⊥} è un’alternativa interessante.

Le clausole per C devono tener conto del nuovo tipo. Se un comando ha come valore OK(s), per qualche s ∈ Store, ciò intuitivamente significa che la sua esecuzione è terminata, non ha provocato errori aritmetici ed s è la memoria finale. Se, invece, il valore di un comando è ER(s), l’esecuzione è stata interrotta per un errore aritmetico; s è la memoria immediatamente precedente al verificarsi dell’errore. Le clausole sono complicate dai test preventivi sulla memoria data come argomento (se si tratta di ER(s), tale valore viene propagato). Per non appesantire ulteriormente la notazione, si identificheranno gli elementi di ResStore con le loro immagini in ResStore_{⊥}.

C[[skip]]  = \underline{λ}s.s
C[[X := a]]  = \underline{λ}s.case s of

ER(s′).ER(s′) |

OK(s′).case A[[a]]s′ of

e(err).ER(s′) |
v(n).OK(s′[n/X])

end

C[[c_{1}; c_{2}]]  = C[[c_{2}]] ∘ C[[c_{1}]]
C[[if b then c_{1} else c_{2}]] = \underline{λ}s. esercizio

C[[while b do c end]] = fix(λf ∈ ResStore_{⊥} → ResStore_{⊥}.\underline{λ}s.

case s of ER(s′).ER(s′) | OK(s′).case B[[b]]s′ of

e(err).ER(s′) |

v(true).f(C[[c]]OK(s′)) |

v(false).OK(s′)

end end)

È istruttivo confrontare la clausola precedente con quella standard di IMP:

C[[while b do c end]] = fix(λf ∈ Store_{⊥} → Store_{⊥}.\underline{λ}s.
COND(B[[b]]s, f(C[[c]]s), s)).

Esercizio: Calcolare il valore di C[[while true do skip]].

Esercizio: Dimostrare che, per ogni comando c e ogni s ∈ Store, C[[c]]ER(s) = ER(s). (Suggerimento: induzione su c).

Esercizio: Dare le clausole semantiche per la funzione C′ col tipo

C′ : Com → Store → ResStore_{⊥}

in modo tale da avere, per ogni s ∈ Store

C[[c]]OK(s) = C′[[c]]s.

(Suggerimento: Uno dei casi più delicati è la sequenzializzazione, che può essere definita nel modo seguente:

C′[[c_{1}; c_{2}]] = λs.let r ⇐ C′[[c_{1}]]s in

case r of

ER(s′).ER(s′) |
OK(s′).C′[[c_{2}]]s′

end

Un trattamento analogo è necessario nel funzionale usato per definire il valore del comando while.)

Esercizio: Dalla clausola per C′[[c_{1}; c_{2}]] possiamo distillare la definizione della funzione

check : [[Store → ResStore_{⊥}] → [ResStore_{⊥} → ResStore_{⊥}]
check = λf ∈ [Store → ResStore_{⊥}].\underline{λ}s ∈ ResStore_{⊥}.
case s of
ER(s′).ER(s′) |
OK(s′).f(s′)
end.

Si riformulino le clausole per C′ usando la funzione check.

Esercizio: Si definisca la semantica di un costrutto stop, la cui semantica informale sia quella di fermare l’esecuzione. È possibile definire un tale costrutto in IMP senza errori?

Esercizio: Si diano clausole semantiche per IMP sia con errori che con blocco espressione.

2.1 Gestori di errori ed eccezioni

La presenza nel linguaggio di un meccanismo di generazione di errori espliciti permette anche, in certi limiti, la gestione di alcune condizioni di errore. Sebbene una trattazione semantica esauriente di eccezioni e loro gestione esuli dallo scopo introduttivo del corso di Metodi, possiamo vedere a titolo d’esempio alcuni semplici casi.

Il primo è quello del costrutto stop dell’esercizio precedente. Si osservi che si tratta, pur nella sua semplicità, di un costrutto di trasferimento del controllo non all’istruzione seguente, ma al termine del programma. Possiamo sfruttare la proprietà C[[c]]ER(s′) = ER(s′) per ogni comando c per simulare questo trasferimento incondizionato del controllo:

C[[stop]] = \underline{λ}s.case s of

ER(s′).ER(s′) | OK(s′).ER(s′) end

Un altro costrutto interessante, che permette di “intrappolare” una condizione di errore è

exec c on error c_{1}

la cui semantica informale è: “esegui c, a meno che la sua esecuzione non generi errore; in tal caso esegui c_{1} nella memoria in cui c si è interrotto”.

C[[exec c onerror c_{1}]] = = \underline{λ}s.case s of

ER(s′).ER(s′) | OK(s′).case C[[c]]s of

ER(s′′).C[[c_{1}]](OK(s′′)) |
OK(s′′).OK(s′′)

end

Esercizio: Si dia la semantica denotazionale del comando

if error on a then c_{1} else c_{2}

la cui semantica informale è “valuta l’espressione a; se la valutazione genera un errore, esegui c_{1}, altrimenti esegui c_{2}”. Possiamo poi definire comandi il cui unico scopo è quello di generare un errore:

raise x := a

dove x è una locazione ed a è un’espressione, con la seguente semantica informale: “valuta l’espressione a; se la valutazione genera un errore, propaga l’errore nella memoria corrente; altrimenti assegna tale valore ad x e genera un errore”. Una possibile clausola semantica per raise è

C[[raise x := a]] = = \underline{λ}s.case s of

ER(s′).ER(s′) |

OK(s′).case A[[a]]s′ of

e(err).ER(s′) |
v(n).ER(s′[n/x])

end

La presenza in un linguaggio di raise e exec-on-error permette una gestione delle eccezioni abbastanza raffinata. A titolo d’esempio, mostriamo che usando questi due costrutti possiamo simulare il costrutto exit loop la cui semantica informale è l’uscita dal while corrente (o un errore se non si è all’interno di alcun ciclo). Assumiamo, per cominciare, di avere a disposizione una locazione err non usata altrimenti nel programma; la prima istruzione della nostra simulazione sarà

err := 0;

Simuleremo ora ogni ciclo della forma

while b do (… exit; …)

con

exec

while b do (… raise err := 1; …) on error

if err = 0 then raise err := 0

else err := 0

3 Esercizi

Notazione: il simbolo ≡ indica la congruenza indotta dalla semantica denotazionale.

1. Nel contesto del linguaggio IMP, si dia la semantica denotazionale di un comando w2 che verifichi la seguente relazione, per ogni BExpr b ed ogni Com c:

w2 b do c ≡ if b then c; w2 b do c; w2 b do c else skip  (2)

e si dica se tale semantica sia maggiore, minore, uguale ovvero inconfrontabile con quella del comando while. Sol. La clausola denotazionale per w2 si ottiene subito dalla (2):

C[[w2 b do c]] = fix H
H = λf.λs.COND(B[[b]]s, f(f(C[[c]]s)), s).

Dimostriamo ora che w2 è un punto fisso del funzionale G che dà la semantica di while b do c. Il calcolo può sfruttare il fatto che ≡ è una congruenza:

w2 c do b ≡ {(2)}
if b then c; w2 b do c; w2 b do c

else skip

≡ {(2)}
if b then c; w2 b do c; if b then c; w2 b do c; w2 b do c else skip

else skip

≡ {∀s ∈ Store_{⊥} C[[w2 c do b]]s ≠ ⊥ ⇒ B[[b]](C[[w2 c do b]]s) = false}
if b then c; w2 b do c

else skip

Ne segue che

C[[while b do c]] ≤ C[[w2 b do c]],

essendo il valore del while il minimo punto fisso di G. Rimane da dimostrare la proprietà usata nella derivazione precedente. La si ottiene dimostrando, con un’induzione di punto fisso rispetto ad H, la seguente proprietà:

P (f) ≡ ∀s ∈ Store_{⊥}.fs ≠ ⊥ ⇒ B[[b]](fs) = false.

Base: P (⊥) è vacua (la premessa dell’implicazione è falsa). Passo induttivo: supponiamo P (f) e dimostriamo P (Hf), ovvero

COND(B[[b]]s, f(f(C[[c]]s)), s) ≠ ⊥ ⇒ B[[b]](COND(B[[b]]s, f(f(C[[c]]s)), s)) = false.

Assumiamo dunque la premessa e ragioniamo per casi: se B[[b]]s = false la tesi è ovvia. In caso contrario, la premessa diviene f(f(C[[c]]s)) ≠ ⊥, da cui, per ipotesi induttiva, la tesi. Proviamo ora che

C[[w2 b do c]] ≤ C[[while b do c]],

mostrando che C[[while b do c]] soddisfa la (2). Posto w = C[[while b do c]], si ha

H(w)s = COND(B[[b]]s, w(w(C[[c]]s)), s)
= COND(B[[b]]s, COND(B[[b]](w(C[[c]]s)), …, w(C[[c]]s)), s)
= COND(B[[b]]s, w(C[[c]]s), s)
= ws.

La terza uguaglianza usa una proprietà di while analoga a quella dimostrata per w2, che può essere stabilita per induzione di punto fisso relativamente al funzionale G. Segue dunque che w2 e while hanno la stessa semantica.

2. Nel contesto del linguaggio IMP, si dia la semantica denotazionale di un comando w2 che verifichi la seguente relazione, per ogni BExpr b ed ogni Com c:

w2 b do c ≡ if b then c; w2 b do (c; c) else skip .  (3)

Si diano poi regole di semantica operazionale strutturata per lo stesso comando e si dimostri l’equivalenza delle due semantiche. Sol. La definizione della semantica denotazionale non è immediata, in quanto, in accordo alla (3), il comando che viene iterato cambia da un’iterazione a quella successiva (prima c, poi c; c, poi c; c; c; c, …). Il funzionale deve avere un ulteriore parametro, che, intuitivamente, rappresenta il “corpo” del ciclo. Formalmente:

C[[w2 b do c]] = (fix H)C[[c]]
H = λf ∈ [Store_{⊥} → Store_{⊥}] → [Store_{⊥} → Store_{⊥}].
λK ∈ [Store_{⊥} → Store_{⊥}].λs ∈ Store_{⊥}.
COND(B[[b]]s, f(K ∘ K)(Ks), s).

Le regole di semantica operazionale sono:

\frac{< b, s >→ true < c, s >→ s_{1} < w2 b do (c; c), s_{1} >→ s_{2}}{< w2 b do c, s >→ s_{2}}

e

\frac{< b, s >→ false}{< w2 b do c, s >→ s.}

L’equivalenza da dimostrare assume la forma seguente:

∀s ∈ Store < c′, s >→ s′ ⟺ C[[c′]]⌊s⌋ = ⌊s′⌋

L’implicazione da sinistra a destra si stabilisce per induzione sulla derivazione senza grossi problemi (il solo caso da mostrare è, ovviamente, quello relativo a w2). Da destra a sinistra ragioniamo per induzione sulla struttura di c. L’unico caso caso che deve essere mostrato è quello in cui c′ è w2 b do c. Trattiamo questo caso con un’ulteriore induzione, sugli approssimanti di fix H; la scelta dell’asserto induttivo non è, ancora una volta, del tutto ovvia. Dimostreremo, per induzione matematica su r, la seguente proprietà, dove si è posto c^{k} per il comando c; …; c, con k volte c:

∀k ∈ Nat ∀s, s′ ∈ Store H^{r}(C[[c^{k}]])⌊s⌋ = ⌊s′⌋ ⇒ < w2 b do c^{k}, s >→ s′.  (4)

La base (r = 0) è ovvia: H^{0} = ⊥ e la premessa della (4) è falsa. Supponiamo dunque vera la (4) per r e dimostriamola per r + 1. Assumiamo che

\begin{aligned}H^{r+1}(C[[c^{k}]])⌊s⌋ & = & COND(B[[b]]⌊s⌋, H^{r}(C[[c^{k}]] ∘ C[[c^{k}]])(C[[c^{k}]]⌊s⌋), ⌊s⌋) \\ & = & ⌊s′⌋ \end{aligned}

e ragioniamo per casi sul valore della condizione booleana. Se B[[b]]⌊s⌋ = false, si ha ⌊s′⌋ = ⌊s⌋; dall’equivalenza tra semantica denotazionale ed operazionale per le espressioni booleane si ottiene < b, s >→ false, da cui la regola per w2 permette di concludere < w2 b do c^{k}, s >→ s. Se, invece, B[[b]]⌊s⌋ = true, si ha (oltre a < b, s >→ true) che

\begin{aligned}⌊s′⌋ & = & H^{r}(C[[c^{k}]] ∘ C[[c^{k}]])(C[[c^{k}]]⌊s⌋) \\ & = & H^{r}(C[[c^{2k}]])(C[[c^{k}]]⌊s⌋). \end{aligned}

Si osservi ora che tutte le funzioni in gioco sono strette (a rigore questo dovrebbe essere dimostrato a parte con un’altra induzione): ne segue che C[[c^{k}]]⌊s⌋ non può essere ⊥, ovvero C[[c^{k}]]⌊s⌋ = ⌊s_{0}⌋, per qualche s_{0} ∈ Store. L’ipotesi induttiva (dell’induzione su r) permette allora di derivare < w2 b do c^{2k}, s_{0} >→ s′. D’altra parte, l’ipotesi induttiva dell’induzione strutturale sui comandi permette di concludere < c^{k}, s >→ s_{0}. Mettendo insieme le derivazioni operazionali che abbiamo stabilito, possiamo concludere, per la regola di w2, che < w2 b do c^{k}, s >→ s′, che è la tesi.