Semantica Operazionale

Elementi di semantica
operazionale
1
Sintassi e semantica
 un linguaggio di programmazione, come ogni sistema formale, possiede

una sintassi
• le formule ben formate del linguaggio (o programmi sintatticamente
corretti)

una semantica
• che assegna un significato alle formule ben formate
• dando un’interpretazione ai simboli
– in termini di entità (matematiche) note
2
Sintassi e semantica
 la teoria dei linguaggi formali fornisce i formalismi di specifica
(e le tecniche di analisi) per trattare gli aspetti sintattici
 per la semantica esistono diverse teorie
 le più importanti sono la semantica denotazionale e la
semantica operazionale
 la semantica formale viene di solito definita su una
rappresentazione dei programmi in sintassi astratta
 invece che sulla reale rappresentazione sintattica concreta
3
Semantica operazionale
• lo stile di definizione tradizionale è quello dei sistemi di transizione
• insieme di regole che definiscono
•
attraverso un insieme di relazioni di transizione
come lo stato cambia per effetto dell’esecuzione dei vari costrutti
• una tipica regola descrive la semantica di un costrutto sintattico c
eseguito nello stato s, specificando il nuovo stato s’ e/o il valore
calcolato v
• i domini semantici con cui rappresentiamo lo stato ed i valori
dipendono dal linguaggio di programmazione
4
Linguaggio Didattico
 Semplice linguaggio imperativo (frammento
di C), blocchi, puntatori, chiamata di
funzione
 Rivediamo l’interprete presentato a
Programmazione I
5
Sintassi concreta
Programma::= int main() {StmtList}
StmtList ::= Stmt ; StmtList | e
Stmt::=Decl | Com
Comandi
Com::=Ide=Exp |
Assegnamento
if (Exp) Com else Com |
Condizionale
while (Exp) Com |
Iteratore
{StmtList} |
Blocco
Ide(Exp) |
Invocazione di fun
return Exp
Calcolo dei risultato di una fun
Espressioni
Exp::= Ide |
Identificatore
Costante |
Costante
Exp Op Exp |
Operazioni Binarie
Uop Exp |
Operazioni Unarie
Ide(Exp) |
Chiamata di fun
(Exp)
Parentesi
Espressioni 2
Ide::= Lettera (Lettera | Cifra | Simbolo)*
Costante::= Numero | Carattere
UnOp::= ! | * |
Op::=+ | - | * |...& | > | < | ==....
Numero::=É
Puntatori
 ! si applica per semplicita’ ai soli identificatori. La
locazione calcolata, in questo caso `e la locazione in
cui `e memorizzato il valore dell’identificatore
 * che si applica ad una qualunque espressione, la
calcola ottenendo un valore v che viene per`o
trasformato in una locazione l. Il valore finale
calcolato `e il valore v’ contenuto nella locazione l.
Dichiarazioni
Decl ::=
Type Ide [=Exp] |
FunctDec
variabile
funzione
FunctDec::= Type Ide (Formal) {StmtList}
Type::= int
Formal::= Type Ide
Nota
 Per semplicita’ si considerano funzioni che
hanno un solo parametro formale
 L’estensione a piu’ parametri e’ banale
 Ricordiamo che il passaggio dei parametri
e’ per valore
Semantica Operazionale
 Domini dei valori
 Componenti dello stato
 Regole di Transizione per ogni categoria
sintattica (espressioni, dichiarazioni,
comandi,programmi)
Domini semantici: lo stato
 in un qualunque linguaggio ad alto livello, lo stato
deve comprendere una componente chiamato
ambiente (environment)
 per modellare l’associazione tra gli identificatori
ed i valori che questi possono denotare (dval)
 il nostro frammento è imperativo ed ha la nozione di
entità modificabile, cioè le variabili ed i puntatori
(create con le dichiarazioni e modificate con
l’assegnamento)
 è quindi necessario un secondo componente dello
stato, chiamato memoria (store)
 per modellare l’associazione fra locazioni e valori
che possono essere memorizzati (mval)
14
L’ambiente
 Per modellare i blocchi l’ambiente e’ una
pila di Frames
• La politica FIFO permette di catturare la
dichiarazione piu’ recente di una variabile
Valori (memorizzabili)
 Ide identificatori
 Val=Int + {omega}+{Undef}
 Loc le locazioni di memoria, possono essere
rappresentati come numeri naturali. Nel seguito
useremo la notazione 0L , 1L , 2L ...ecc, per indicare
rispettivamente le locazioni di indirizzo 0, 1, 2 ecc
Memoria
• store: Loc ---> Val
(si usa la metavariabile μ)
 Nota: Val non contiene le locazioni. Nella
semantica data, si usano meccanismi per
trasformare locazioni in valori e viceversa. La
seconda `e possibile ed anzi molto semplice
perch`e le locazioni sono numeri naturali
Frame
• frame: Ide ---> Den
(si usa la metavariabile φ)
 Den = Loc ∪ FunDecl ∪ Unbound.
L’insieme delle denotazioni `e l’unione
dell’insieme Loc degli indirizzi di memoria e
dell’insieme FunDecl delle definizioni di
funzione e della denotazione speciale Undef,
che rappresenta una situazione di errore.
Funzioni
FunDecl `e una tripla
Ide × SList × Env
1) il nome del parametro formale
2) il corpo della funzione
3) l’ambiente di definizione (scoping
statico)
Operazioni sui Frames
 EmptyFrame crea il frame ovunque
indefinito
φ(x)=Unbound per ogni x
Modifica di un frame
φ[d/x](y)= φ(y) se x e’ diverso da y
d se x=y
• La definizione cos`ı data risulta corretta
anche nell’eventualit`a che un legame diverso
da Unbound per x esista gia’
• non e’ molto corretto solo per programmi
sintatticamente corretti
Ambiente
• env=Stack(Frames)
(si usa la metavariabile σ)
Operazioni sulla pila
• EmptyStack crea la pila vuota
• top restituisce l’elemento in testa alla pila
ovvero l’ultimo elemento inserito. Non
modifica la pila.
• pop restituisce l’elemento in testa alla pila.
Modifica la pila, eliminando l’elemento in
testa.
• push inserisce un elemento in testa alla pila.
Operazioni sulla memoria
• μ : Loc ---> Val
Val=Int + {omega}+{Undef}
• Verrebbe da dare operazioni analoghe a
quelle del frame....si tratta di una
funzione parziale
Gestione della memoria
• allocazione di memoria: l’inserzione di
nuovi legami nella memoria corrisponde alla
allocazione di memoria su una machina, e
differisce dall’inserzione di un nuovo legame
in un generico frame
• Deve esserci un meccanismo per assegnare una
nuova locazione ancora libera
• Deve esserci un modo per distinguere una
locazione assegnata con valore indefinito da
una libera
Operazioni sulla Memoria
• μ(l)=omega
• μ(l)=Undef
valore speciale
indefinita
 EmptyStore crea una memoria ovunque
indefinita
μ(x)=Undef per ogni x
Allocazione di Memoria
• free: Store---> Loc *Store
• restitituisce una nuova locazione libera e la
memoria modificata di conseguenza
• free(μ) = (μ’,l) dove
μ’(l’)= μ(l’) per ogni l’!= l
μ’(l)=omega se μ(l)=Undef
Modifica di Memoria
μ[v/l](l’)= μ(l’) se l != l’
Undef
se μ(l)=Undef
v altrimenti
 l’operazione di modifica non effettua
l’inserzione del legame per l nel caso non ne
esista alcuno ma in questo ultimo caso, lascia
la memoria invariata (da un punto di vista
matematico va bene....)
Le funzioni di valutazione semantica
 per ogni dominio sintattico esiste una funzione di
valutazione semantica
 E : EXPR * env * store  (eval * store)
 C : COM * env * store  store
 D : DEC * env * store  (env * store)
 P : PROG * env * store  store
29
Implementazione in OCaml
 Vediamo i domini
 La Sintassi Astratta
 Le funzioni di valutazione semantica che
assegnano un significato ai vari costrutti, con una
definizione data sui casi della sintassi astratta
 Per semplicita’ nell’interprete si usano funzioni
che restituiscono una coppia (ambiente, memoria)
per ogni categoria sintattica
Programma PicoC
 http://www.di.unipi.it/~occhiuto/PicoC/
 Generatore di programmi PicoC in
sintassi astratta
 Alcuni esempi di programmi PicoC in
sintassi astratta per testare l`interprete
Valori
Val=Int + {omega}+{Undef}
type value =
Val of int |
Omega |
Undef;;
Valori Denotabili
Den = Loc ∪ FunDecl ∪ Unbound
type denotation =
Loc of int |
Funct of string * com * sigma ref |
Unbound;;
•
In FunDecl c’e’ il riferimento all’env (per
trattare la ricorsione ..)
Frame
• frame: Ide ---> Den
(si usa la metavariabile φ)
type fi = Frame of
(string * denotation) list;;
• Definizione molto a basso livello, una lista di
coppie (identificatore, valore)
Ambiente
• env=Stack(Frames)
type sigma = Stack of
fi list;;
• Definizione molto a basso livello, una lista di
frames
Memoria
• μ : Loc ---> Val
 type 'a mu = Mem of 'a list ;;
• Definizione molto a basso livello, una lista
polimorfa
• Si usera’ per memorizzare coppie (identificatore,
valore)
Espressioni
 type aop = Add | Sub | Mul | Div | And
| Or | Ls | Gr | Eq ;;
 type unop = Neg | Amp | Star;;
 type aExp = Num of int |
Exp of aExp * aop * aExp |
Bracket of aExp |
UnExp of unop * aExp |
Var of string |
Apply of string * aExp ;;
Comandi
 type com = Assign of string * aExp |
AssignDeRef of aExp * aExp |
If of aExp * com * com |
While of aExp * com |
Block of (stmt list) |
Return of aExp;;
Dichiarazioni
 type decl =
Decl1 of espType * string |
Decl2 of espType * string * aExp |
DeclFun of espType * string * espType *
string * com;;
Programmi
type stmt = StDec of decl |
StCom of com;;
type prog = Prog of (stmt list);;
• Un programma e’ una lista di statements
(dichiarazioni, comandi)
Funzione main
 let valProg (Prog l)=
let (sigma,mu)=
valStmtL l (Stack[Frame[]],(Mem []))in
(mu,sigma);;
• Il programma e’ valutato nello stato iniziale,
lo stack contiene un frame vuoto e la
memoria e’ vuota
• restituisce lo stato ottenuto
Per valutare una lista di
statements
 Funzione ricorsiva (valStmtL)
 Per ogni statement (comando o
dichiarazione) chiama la funzione di
valutazione corrispondente
Lista di Statements
let valStmtL l (sigma, mu) =
match l with|
[] -> (sigma, mu)|
st::stml ->
(match st with
| StDec d -> let (sigma1, mu1) = valDecl d
(sigma,mu)
in valStmtL stml (sigma1,mu1)
|
StCom c -> let (sigma1,mu1) = valCom c
(sigma,mu)
in valStmtL stml (sigma1,mu1));;
Dichiarazioni
 valDecl:
Decl * (env*mem)---> (env*mem)
 Funzione ricorsiva (valDecl)
 Usa valExp:
Exp* (env*mem)---> (Val*env*mem)
Dichiarazioni
 Variabile senza inizializzazione
 Variabile con inizializzazione
 Funzione
Sintassi Astratta
 type decl =
Decl1 of espType * string |
Decl2 of espType * string * aExp |
DeclFun of espType * string * espType *
string * com;;
Funzioni Ausiliarie: memoria
• free: Store---> Loc *Store
• restitituisce una nuova locazione libera e la
memoria modificata di conseguenza (alla nuova
locazione viene assegnato il valore omega)
type 'a mu = Mem of 'a list ;;
Implementazione
let free (Mem xm) = let loc = (length xm)
in
((Loc loc),
(Mem (append xm [((Loc loc),Omega)]
)));;
• la lista e’ del tipo [(0,v1),(1,v20)...]
• la prima locazione libera e’ detreminata con
length
Modifica della Memoria
 Serve una operazione
updateM:Store*Loc*Val---> Store
• Modifica la memoria rimpiazzando il
valore associato alla locazione con il
nuovo valore
Implementazione
let rec updateM (Mem m) (x,y) = let def m x = foldr
(or) false (map (compose ((=) x) (fst)) m)
and modify m (x,y) = let f (x,y) b = if ((fst b)=x)
then (x,y) else b
in map (f(x,y)) m
in if (not(def m
x)) then (Mem m) else (Mem (modify m (x,y)));;
Usa due funzioni ausiliarie def e modify per
testare se la locazione x e’ definita e per
modificarne il valore nella lista
Modifica dell’env
let rec addBind sigma (x,y) = match sigma with
| Stack [Frame[]] ->
Stack [Frame[(x,y)]]
| Stack ((Frame f)::fs) ->
Stack ((Frame (append f [(x,y)])) ::fs);;
• inserisce il nuovo legame tra x ed y nell’env
sigma (ovvero nel frame al top della pila, tramite
append e’ una lista di coppie)
Dichiarazione di variabile
semplice
let valDecl d (sigma,mu) = match d with
Decl1 (t,i) ->
let (l,mu1) = free mu
in let sigma1= (addBind sigma (i, l))
in (sigma1, mu1)
• viene modificata la memoria (l e’ una locazione
fresh, coniene valore indefinito)
• viene modificato l\’env inserendo l’associazione
(i,l)
Dichiarazione di variabile con
inizializzazione
let valDecl d (sigma,mu) = match d with
Decl2 (t,i,e) ->
let (v,(sigma1,mu1)) = (valExp e (sigma,mu))
in let (l,mu2) = free mu1 in
let sigma2= (addBind sigma1 (i,l))
in let mu3 =
updateM mu2 (l, v) in (sigma2, mu3)
• viene modificata la memoria (l e’ una locazione fresh
coniene valore indefinito)
• viene modificato l ’env inserendo l’associazione (i,l)
• il contenuto della locazione l viene poi aggiornato con il
valore calcolato per l’espressione e
Dichiarazione di Funzione
DeclFun (t,i,tp,ip, c)
• stiamo dichiarando una funzione di nome
i,parametro ip, corpo c in (sigma,mu)
• dovremmo modificare l’env sigma
inserendo l’associazione tra i e la sua
descrizione
(ip,c,sigma1)
• chi e’ sigma1? vediamo la regola formale
Problemi di Implementazione
• bisogna implementarlo usando un
puntatore all’env in FunDecl
Funct of string * com * sigma ref |
Unbound;;
Dichiarazione di Funzione
let valDecl d (sigma,mu) = match d with
DeclFun (t,i,tp,ip, c) ->let rec
sigma1=(addBind sigma (i,
(Funct (ip,c, (ref sigma)))))
in ((update i sigma1 sigma1),mu)
• in sigma1 la descrizione della funzione i contiene
un riferimento a sigma (andrebbe bene se non
fossero ricorsive
• nota che viene restituito come risultato
update i sigma1 sigma1
Intuitivamente
update i sigma1 sigma1
• cerca la descrizione di funzione di i in sigma1
(p,c, sigma ref)
• la modifica assegnando sigma1 al posto di sigma
Funzione Ausiliaria
let rec updateF i f sigma = match f with
[] -> f |
(j, Funct(x,c,var))::fs when (i=j) ->
var :=sigma; f
| (_,_)::fs -> updateF i fs sigma;;
let rec update i s sigma = match s with
Stack [Frame[]]-> s |
Stack ((Frame fs)::ss) ->
(updateF i fs sigma); s;;
Comandi
 valCom:
Com * (env*mem)---> (env*mem)
 Funzione ricorsiva (valCom)
 Usa valExp:
Exp* (env*mem)---> (Val*env*mem)
Comandi





Condizionale
While
Assegnamento
Blocco
Return
Comandi
 type com = Assign of string * aExp |
AssignDeRef of aExp * aExp |
If of aExp * com * com |
While of aExp * com |
Block of (stmt list) |
Return of aExp;;
Funzioni Ausiliarie: env
• lookup: Env * Ide---> Den
Den = Loc ∪ FunDecl ∪ Unbound
• restitituisce il valore denotabile
associato all’identificatore
• Env e’ uno Stack di Frames, in realta’ e’ una lista
di frames
• la ricerca ricorsiva inizia dal frame al top, e.g. dal
primo elemento della lista
Funzioni Ausiliarie: frame
• look: Frame * Ide---> Den
Den = Loc ∪ FunDecl ∪ Unbound
• restitituisce il valore denotabile
associato all’identificatore
• Frame e’ una lista di coppie (identificatore,
valore)
Implementazione
let rec lookUp sigma y =
match sigma with
|
Stack [] -> Unbound
|
Stack (x :: xs) -> let b= (look x y)
in if (not (b=Unbound))
then b else (lookUp (Stack xs) y);;
let rec look fi y = match fi with
|
Frame [] -> Unbound
|
Frame ((i, d) :: xs) ->
if (i=y) then d else (look (Frame xs) y);;
Condizionale
let valCom c (sigma,mu) = match c with
| If (e,c1,c2) -> let
((Val i),(sigma1,mu1)) = (valExp e (sigma,mu))
in if not (i=0) then valCom c1 (sigma,mu1)
else valCom c2 (sigma,mu1)
• viene calcolato il valore di e
• se true esegue c1, altrimenti c2
While
let valCom c (sigma,mu) = match c with
| While (e,c) -> let
((Val i),(sigma1,mu1)) = (valExp e (sigma,mu))
in
if not (i=0) then
let (sigma2,mu2) = (valCom c (sigma1,mu1))in
valCom (While (e,c)) (sigma2,mu2)
else
(sigma1, mu1)
• viene calcolato il valore di e, se false restituisce
(sigma1,mu1)
• se true esegue While (e,c) nello stato
modificato da c
Assegnamento
let valCom c (sigma,mu) = match c with
| Assign (s,e) -> let
(v,(sigma1,mu1)) = (valExp e (sigma,mu))
and (Loc l) = (lookUp sigma s) in
(sigma1, updateM mu1 ((Loc l),v)
• viene calcolato il valore v di e e la locazione l
legata alla variabile s in sigma
• viene modificato lo store assegnando alla
locazione l il valore v
Blocco
let valCom c (sigma,mu) = match c with
| Block l ->
let (Stack (f::rl),mu1) =
valStmtL l
((match sigma with Stack fl ->
Stack (Frame[]::fl)) ,mu)
in (Stack rl, mu1)
• valuta l nello stato in cui un frame vuoto Frame[]
e’ stato messo al top della pila
• restituisce l’env da cui e’ stato fatto pop (le
variabili del blocco sono locali)
Blocco: regola astratta
• l’implementazione delle operazioni di pop() e
push(frame) e’ parecchio complicata
• regola astratta
Return
let valCom c (sigma,mu) =
match c with
| Return e ->
valCom (Assign ("retVal",e))
(sigma,mu))
• assegna il valore di e ad una variabile speciale
retval, valore di ritorno della funzione che e’ in
esecuzione
Assegnamento Deferenziato
let valCom c (sigma,mu) = match c with
| AssignDeRef (e,ev) -> let
(v,(sigma1,mu1)) =
(valExp ev (sigma,mu))
in let
(v1,(sigma2,mu2)) =
(valExp e (sigma1,mu1))
in let (Loc l) = (etaLoc v1) in
(sigma2, updateM mu2 ((Loc l),v))
• viene calcolato il valore v di e e il valore v1 di e
• viene modificato lo store assegnando alla
locazione corrispondente a v1 il valore v
Funzione Ausiliaria:
let niLoc x = match x with
(Loc l) -> (Val l)
|_ -> Undef;;
let etaLoc x = match x with
(Val n) when (n>=0) -> (Loc n)
| _ -> Unbound;;
• trasformano locazioni in valori interi e viceversa
Espressioni
 valExpr:
Expr * (env*mem)---> Val *(env*mem)
 Funzione ricorsiva (valExpr)
Espressioni




costanti
valore di una variabile
risultato di una chiamata di funzione
operazioni di confonto, somma tra
espressioni (binarie)
 operazione unaria
Espressioni
 type aop = Add | Sub | Mul | Div | And
| Or | Ls | Gr | Eq ;;
 type unop = Neg | Amp | Star;;
 type aExp = Num of int |
Exp of aExp * aop * aExp |
Bracket of aExp |
UnExp of unop * aExp |
Var of string |
Apply of string * aExp ;;
Funzioni Ausiliarie: stato
• getVal: (Env*Mem) * Ide---> Val
• deve restituire il valore associato
all’identificatore x
• cercare nella pila di Frames Env la locazione l
associata ad x
• restituire il valore associato ad l nella
memoria
Implementazione
let rec getVal (sigma,mu) x =
let b=(lookUp sigma x) in
match b with
|
Loc n -> (lookM mu (Loc n))
| _ -> Undef;;
• lookUp cerca nell’env (pila) la locazione n
associata ad x
• lookM cerca nella memoria il valore associato ad
n
Implementazione:lookM
let rec lookM mu y = match mu with
Mem [] -> Undef
| Mem (( i, v) :: xs) ->
if (i=y) then v else
(lookM (Mem xs) y);;
|
la memoria e’ una lista di coppie (i,v),
cerca ricorsivamente un identificatore
uguale ad y
Costante, Parentesi
let rec valExp e (sigma,mu) = match e
with
| Num n -> ((Val n),(sigma,mu))
| Bracket x
-> valExp x (sigma,mu)
Variabile
let rec valExp e (sigma,mu) = match e
with
| Var s ->
((getVal (sigma,mu) s),(sigma,mu))
• restituisce il valore associato alla
variabile s, calcolato tramite getVal
Operazioni Binarie
let rec valExp e (sigma,mu) = match e
with
| Exp (x, op, y) -> let
(v1, (sigma1,mu1))= (valExp x (sigma,mu))
in let
(v2,(sigma2,mu2))= (valExp y (sigma,mu1))
in...
• calcola ricorsivamente i valore v1 e v2 di
x ed y, rispettivamente
• in un ordine
Procede per casi sull’operazione
if (isNumOp op) then
(niNum ( (funNumOp op) (etaNum v1)
(etaNum v2)),(sigma2,mu2))
else
• isNumOp restituisce true se e’ una operazione
numerica (somma etc..)
• FunNumOp applica l’operazione corrispondente a op
ai valori v1 e v2
• niNum,etaNum servono solo per convertire i valori
Val i in i e viceversa
Funzioni ausiliarie
let
|
|
|
|
|
isNumOp op = match op with
Add -> true
Sub -> true
Div -> true
Mul -> true
_ ->
false;;
Funzioni ausiliarie
let funNumOp op = match op with|
Add -> (+)|
Sub -> (-)|
Mul -> (fun x y -> x*y) |
Div -> (/) ;;
Funzioni ausiliarie di
conversione per interi
let niNum x =
(Val x);;
let etaNum (Val x) = x;;
Procede per casi
if (isBoolOp op) then
(niBool( (funBoolOp op) (etaBool v1)
(etaBool v2)) ,(sigma2,mu2))
else
(niBool( (funRelOp op) (etaNum v1)
(etaNum v2)) ,(sigma2,mu2))
• se e’ un’operazione booleana applica la relativa
operazione ai valori booleani v1 e v2
• se e’ un’operazione relazionale applica la relativa
operazione ai valori booleani v1 e v2
Funzioni ausiliarie
let
|
|
|
isBoolOp op = match op with
And -> true
Or -> true
_ -> false;;
Funzioni Ausiliarie
let funBoolOp op = match op with
| And -> (&)
| Or -> (or) ;;
let funRelOp op = match op with|
Ls -> (<) |
Gr -> (>) |
Eq -> (=);;
Funzioni Ausiliarie di
conversione
let niBool x = if x then
(Val 1) else (Val 0);;
let etaBool (Val x) = if (x=0)
then false else true;;
Operazioni Unarie: per casi
let rec valExp e (sigma,mu) = match e with
| UnExp (op, x) -> (match op with
Neg ->
let
(v1, (sigma1,mu1))= (valExp x (sigma,mu))
in
(niBool( (funop1 op) (etaBool(v1))
),(sigma1,mu1))
 caso della negazione e’ analogo a quello
visto prima
 calcola il valore v di x e chiama funzioni
Operazioni Unarie: puntatore
| UnExp (op, x) -> (match op with
|Amp -> ((valDen x sigma),(sigma,mu))
 deve restituire la locazione di x
 usa una funzione ausiliaria valDen
Funzione ausiliaria:valDen
let rec valDen e sigma = (match e with |Var s ->
niLoc(lookUp sigma s)
|Exp (x,y,z) ->
Undef|UnExp(x,y) -> Undef|
Bracket x -> Undef);;
 e’ definita nel caso di espressione e generica,
ma e’ definita solo per le variabili
 tramite lookup restituisce la locazione associata
ad s nell’ambiente sigma
Operazioni Unarie: deferenziato
| UnExp (op, x) -> (match op with
|Star ->
let (v,(sigma,mu1)) =(valExp x (sigma,mu))
in (lookM mu1 (etaLoc v),(sigma,mu1)))
 calcola il valore v di x (tramite valExp)
 restuisce il valore memorizzato nella
memoria nella locazione v
Chiamata di Funzione
 Apply(s,a) dobbiamo applicare la funzione s al
parametro attuale a nello stato (sigma,mu)
 Parte I: dobbiamo cercare il nome s nell’ambiente
sigma, restituisce un FunDecl
Funct(f,c,sigmaf)
• f e’ il parametro formale
• c e’ il corpo della funzione
• sigmaf e’ l’ambiente al momento della dichiarazione
della funzione s (scoping statico)
 Parte II: dobbiamo valutare il parametro a nello stato
corrente, calcolarne il valore v (per valore)
Chiamata di Funzione:Part II
 Dobbiamo valutare il corpo della funzione c, in quale
stato?
 Lo stato di valutazione si costruisce a partire da
(sigmaf,mu)
• Bisogna mettere sulla pila sigmaf un EmptyFrame
(push) che serve per contenere le dichiarazioni locali
alla funzione
• Le dichirazioni locali conterranno il legame tra il
parametro formale f ed il valore del parametro attuale
v e la variabile speciale retval
• Nota che per inserire un legame devono essere modifica
sia l’ambiente che la memoria
Chiamata di Funzione:Part III
 Cosa restituisce?
 il valore associato alla variabile retval
 l’ambiente sigma al momento della chiamata (non
modificato)
 la memoria modificata dall’esecuzione dei comandi
Chiamata di Funzione: valExp
• Vediamo il codice di valExp per la funzione
• Molto complicato, perche’ di basso livello
• La nozione di stato (env,mem) non fornisce operazioni
chiare per fare push, pop
• Inoltre l’introduzione di un nuovo legame in un frame
viene fatto a mano, operando direttamente sulla lista
che implementa il frame
• Analogamente l’introduzione di un nuovo legame nella
memoria viene fatto a mano, operando direttamente
sulla lista che lo implementa
Chiamata di funzione
let rec valExp e (sigma,mu) = match e
with
| Apply (s,a) ->
let
(v,(sigma1,mu1))=
valExp a (sigma,mu) in
(match (lookUp sigma s) with
Funct (f,c, sigmaf) ->
....
• calcola tramite valExp il valore v del parametro
attuale a
• cerca tramite lookUp la FunDecl relativa ad s
Chiamata di funzione
(let (l,mu2)=(free mu1) in let (l1,mu3)
=(free mu2)
in let
sigmav=(match (! sigmaf) with
Stack sl ->
addBind (addBind (Stack
(Frame []::sl)) (f,l)) ("retVal",l1))
• sceglie due locazioni libere in memoria l ed l1
• modifica l’ambiente sigmaf , facendo push di
un frame che contiene (f,l) e (retval l1)
Chiamata di funzione
in let (sigma2,mu4)=
valCom c (sigmav,updateM mu3 (l, v))
in ((lookM mu4 l1),(sigma,mu4)))
• valuta il corpo della funzione c nell’ambiente sigmav
costruito in precedenza,e nella memoria ottenuta
aggiungendo il legame tra (l,v)
• restituisce il valore della locazione l1 nella memoria (il
valore di retval), l’ambiente sigma iniziale, e la
memoria finale mu4