Semantica Operazionale Strutturata
Semantica per riscrittura o riduzione o semplificazione basata sulla
struttura dei termini che voglio semplificare
Si individuano dei termini (del linguaggio) che rappresentano
direttamente dei valori, cioè che non possono essere ulteriormente
semplificati.
Si danno delle regole di semplificazione in modo tale che ogni termine
corretto si riduca ad uno e uno solo di quei termini che rappresentano
valori
In realtà come nel caso denotazionale abbiamo bisogno di ambienti e
stati per poter eseguire le semplificazioni.
Quindi la semplificazione agisce su configurazioni, che consistono di
un termine e del contesto in cui si vuole valutare il termine.
SOS a grandi passi per LW
Molto simile alla semantica denotazionale
Come configurazioni usiamo
Conf = L  Env  States
Gli stessi della denotazionale
tranne che cambia Value
[T] è l’insieme dei valori sintattici di tipo
T: [int] = {0,1,2,..-1,-2….}, [bool] =
{true,false}
Definiamo la semplificazione come relazione binaria sulle configurazioni:
  Conf  Conf
L = sN Ls(LW)  {l}  {*}
Siccome la maggior parte delle semplificazioni non modifica gli ambienti
introduciamo una notazione semplificata:
(t,s) r (t’,s’) sse (t,r,s)  (t’,r,s’)
Una configurazione (t,r,s) è finale se
t = l (ho rielaborato tutto il termine in esame usandolo per modificare ambiente e/o stato) o
t Value+ (ho raggiunto un termine che rappresenta un valore)
A grandi passi vuol dire che se derivo (t,r,s)  (t’,r,s’), allora (t’,r,s’) è finale (non
vado mai in uno stato intermedio, ma direttamente alla fine)
Espressioni
Denotazionale
[e] (r,s) = (v,s’)
[es] (r,s’) = (lv,s”)
[e es] (r,s) = (v lv,s”)
r(x) LocT
SOS a grandi passi
[x](r,s) = (s(r(x)),s)
(e,s) r (v,s’)
(e es, s) r (v lv,s”)
r(x) LocT
[es](r,s) = (lv ,s’)
[f(es)](r,s) = r(f)(lv,s’)
(x,s) r (s(r(x)),s)
(e,s) r (v,s’)
[e](r,s) = (v ,s’)
[x = e](r,s) = (v,s’[v/r(x)])
(es,s’) r (lv,s”)
(x=e,s) r (v,s’[v/r(x)]))
a è la rappresentazione
sintattica del valore
ottenuto sommando i
valori rappresentati da
v e v’
(es,s) r (lv,s’)
(f(es),s) r r(f)(lv,s’)
[e] (r,s) = (v,s’) [e’] (r,s’) = (v’,s”)
(e,s) r (v,s’) (e’,s’) r (v’,s”)
v + v’ =a
v + v’ =a
[e + e’] (r,s) = (a,s”)
(e+e’,s) r (a,s”)
Espressioni completamento
In realtà bisogna anche aggiungere tutti i controlli di tipo
Alcuni controlli
si possono
omettere in
quanto derivano
dalla grammatica
CF
Altri esprimono
proprio il fatto
che stiamo
dando una
semantica a
grandi passi
eLExp(LW)
vValue
esLExps(LW)
lv Value+
(e,s) r (v,s’)
(e es, s) r (v lv,s”)
r(x) LocT
xLId(LW)
eLExp(LW)
vValue
xLId(LW)
fLId(LW)
esLExps(LW)
lv Value+
(es,s’) r (lv,s”)
(x,s) r (s(r(x)),s)
(e,s) r (v,s’)
(x=e,s) r (v,s’[v/r(x)]))
(es,s) r (lv,s’)
(f(es),s) r r(f)(lv,s’)
Dichiarazioni di variabili
Denotazionale
[d] (r,s) = (r’,s’)
SOS a grandi passi
[ds] (r’,s’) = (r”,s”)
[d ds (r,s) ] = (r”,s”)
dLDec(LW)
(d,r,s)  (l,r’,s’) (ds,r’,s’)  (l,r”,s”)
dsLDecs(LW)
(d ds,r,s)  (l,r”,s”)
Nuova(l,r,s)
[t x](r,s) = (r[l/x],s[/l])
Nuova(l,r,s)
xLId(LW)
tLType(LW)
Nuova(l,r,s’)
(t x,r,s)  (l, r[l/x],s[/l])
[e](r,s) = (v ,s’)
[t x = e](r,s) = (r[l/x],s’[v/l])
Nuova(l,r,s’)
eLExp(LW)
xLId(LW)
tLType(LW)
(e,s) r (v,s’)
(t x = e,r,s)  (l, r[l/x],s’[v/l])
Dichiarazioni di funzioni ricorsive: void
(void f(T x) {sts},r,s)  (l, r[F/f],s)
[void f(T x) {sts}](r,s) = (r[F/f],s)
Dove F : [T]  States  {*}  States
è definita induttivamente da tutte le regole della semantica più le seguenti due:
[sts] (r[/f,l/x],sc[v/l]) = s’
F(v,sc) = (*,s’-{l})
[e](r[/f],s1) = (u ,s’)
Nuova(l,r,sc)
F(u,s’) = (*,s”)
[f(e)] (r[/f],s1) = (*,s”)
(sts, sc[v/l]) r[/f,l/x] (l, s’)
F(v,sc) = (*,s’-{l})
(e, s1) r[/f] (u, s’)
F(u,s’) = (*,s”)
(f(e), s1) r[/f] (*,s”)
Dichiarazioni di funzioni ricorsive: BType
[RT f(T x) {sts result e}](r,s) = (r[F/f],s)
(RT f(T x) {sts result e},r,s)  (l, r[F/f],s)
Dove F : [T]  States  [RT]  States
è definita induttivamente da tutte le regole della semantica più le seguenti due:
[sts] (r[/f,l/x],sc[v/l]) = s’ [e](r[/f,l/x], s’)= (a ,s”)
F(v,sc) = (a,s”-{l})
(sts, sc[v/l]) r[/f,l/x] (l, s’) (e, s’) r[/f,l/x] (a, s”)
Nuova(l,r,sc)
Nuova(l,r,sc)
F(v,sc) = (a,s”-{l})
[e](r[/f],s1) = (u ,s’) F(u,s’) = (a ,s”)
[f(e)] (r[/f],s1) = (a ,s”)
(e, s1) r[/f] (u, s’)
F(u,s’) = (a,s”)
(f(e), s1) r[/f] (a, s”)
Statements 1
[st] (r,s) = s’
[sts] (r,s’) = s”
[st sts ] (r,s) = s”
stLStat(LW) (st, s) r (l, s’)(sts, s’) r (l, s”)
stsLstats(LW)
(st sts, s) r (l, s”)
[e](r,s) = (v ,s’)
[e;](r,s) = s’
[e](r,s) = (tt ,s’)
[sts] (r,s’) = s”
[if (e) {sts} else {sts’}](r,s) = s”
[e](r,s) = (ff ,s’)
[sts’] (r,s’) = s”
[if (e) {sts} else {sts’}](r,s) = s”
eLExp(LW)
(e, s) r (v, s’)
(e;, s) r (l, s’)
(e, s) r (true, s’)
(sts, s’) r (l, s”)
(if (e) {sts} else {sts’}, s) r (l, s”)
(e, s) r (false, s’) (sts’, s’) r (l, s”)
(if (e) {sts} else {sts’}, s) r (l, s”)
Statements 2: while
(e, s) r (false, s’)
[e](r,s) = (ff ,s’)
[while (e) {sts}](r,s) = s’
[e](r,s) = (tt ,s’)
[sts] (r,s’) = s”
(while (e) {sts}, s) r (l, s’)
[while (e) {sts}](r,s”) = s0
[while (e) {sts}](r,s) = s0
(e, s) r (true, s’) (sts, s’) r (l, s”)
(while (e) {sts}, s”) r (l, s0)
(while (e) {sts}, s) r (l, s0)
Problema dei valori
Consideriamo la semantica dell’espressione 3 + 2.
Per valutarne la semantica possiamo solo usare la regola della somma
(3+2,s) r (5,s”)
(3,s) r (v,s’)
(2,s’) r (v’,s”)
______ ____ ____
______
______ ____ ____
______
?
?
?
?
?
v + v’ =5
?
Non ci sono regole per completare alberi di questa forma.
In realtà in tutte le regole (che ce l’hanno) la valutazione di
un’espressione dovrebbe essere opzionale, perché se l’espressione è già
un valore non va ulteriormente elaborata.
Quindi, ad esempio, ci vorranno regole tipo
(e,s) r (v,s’)
(e+v’,s) r (a,s’)
v + v’ =a
(e’,s) r (v’,s’)
(v+e’,s) r (a,s’)
(while (false) {sts}, s) r (l, s)
(v;, s) r (l, s)
v + v’ =a
(v+v’,s) r (a,s)
v + v’ =a
Nuova(l,r,s’)
eLExp(LW)
xLId(LW)
tLType(LW)
(t x = v,r,s)  (r[l/x],s[v/l])
Relazione con la semantica denotazionale
Le due semantiche coincidono, fatti i dovuti aggiustamenti tecnici,
cioè adeguate le due notazioni:
[d]Decs(r,s)=(r’,s’) se e solo se (d,r,s)  (l, r’, s’)
[st]Stats (r,s)=s’ se e solo se (st,s) r (l, s’)
[e]Exps(r,s)=(v,s’) se e solo se (e,s) r (v, s’)
e modulo una traduzione fra i valori (usati nella semantica
denotazionale) e le loro descrizioni sintattiche (usate nella
semantica operazionale)
Non sono necessarie prove, o meglio la prova è banale, perché le
due semantiche sono descritte da regole “isomorfe” (a volta
partizionate in modo diverso, a seconda che le espressioni coinvolte già
rappresentino valori)
Quindi i due approcci hanno gli stessi limiti.
In particolare, non danno informazioni in caso di non terminazione.
Questo può essere riduttivo in caso di sistemi che sono progettati in
modo non terminante (e.g. sistemi operativi)