Semantica Operazionale di un
frammento di Java: lo stato
estensione (con piccole varianti) di quella in
Barbuti, Mancarella, Turini,
Elementi di Semantica Operazionale,
appunti di Fondamenti di Programmazione
1
Semantica operazionale
 modello di esecuzione
– importanti soprattutto le strutture che
compongono lo stato
 simile alle strutture a run-time della JVM,
che esegue il byte-code prodotto dal
compilatore
– con alcune semplificazioni legate alle
ottimizzazioni effettuate dal compilatore
2
Cosa aggiungiamo
 le gerarchie di classi
– trattiamo l’ereditarietà ed l’overriding
 l’attributo “static” per variabili e metodi
– esistono variabili e metodi propri della classe
 i costruttori
– metodi che vengono invocati al momento della
creazione di una istanza di classe
3
Semantica statica
 nella formalizzazione trascuriamo tutti gli aspetti
legati alla semantica statica
– in particolare, quelli che darebbero origine a messaggi
di errore durante la compilazione
– tipi, visibilità dei nomi, vincoli sull’overriding
 le proprietà statiche importanti verranno descritte
in modo informale
 semantica semplificata solo per programmi che
supererebbero con successo l’analisi statica
4
Lo stato
 pila di attivazioni s
– per la valutazione dei metodi
– simile alla pila dei record di attivazione nei linguaggi
tradizionali
 heap z
– contiene gli oggetti (istanze di classi)
 ambiente delle classi r
– contiene le classi dichiarate prima dell’inizio
dell’esecuzione
5
Ambiente delle classi r
 r è una funzione da identificatori di classe a
descrizioni di classe
– r : Cenv
– Cenv = Id -> Cdescr
 cos’è una descrizione di classe?
 vediamo prima la sintassi (semplificata) che
usiamo per le dichiarazioni di classe
6
Dichiarazione di classe: sintassi
Class_decl := class Id extends Id {
Static_var_decl_list
Static_meth_decl_list
Inst_var_decl_list
Inst_meth_decl_list
Costruttore
}
Cdescr = Id * Frame * Menv * Frame * Menv
superclasse
variabili istanza
variabili statiche
metodi istanza
metodi statici
il costruttore (sequenza di assegnamenti) viene aggiunto ai metodi istanza
7
Il frame
 è una tabella (estendibile e mutabile) che mantiene
associazioni fra
– identificatori (di variabili)
– valori
• interi, booleani
• locazioni (puntatori ad oggetti)
 un frame j:Frame viene creato vuoto (newframe())
 l’operazione bind(j, i, v) estende j inserendo l’associazione tra i e v
 l’operazione update(j, i, v) modifica in j l’associazione per i (che
deve esistere)
 l’operazione defined(j, i) dice se j contiene un’associazione per i
 per ottenere il valore di una variabile, si applica il frame all’Id
8
Ambiente di metodi m
 m è una funzione da identificatori di metodo a
descrizioni di metodo
– m : Menv
– Menv = Id -> Mdescr
 cos’è una descrizione di metodo?
 vediamo prima la sintassi (semplificata) che
usiamo per le dichiarazioni di metodo
9
Dichiarazione di metodo: sintassi
Method_decl := Id (Idlist) Blocco
– ignoriamo i tipi
– quando il metodo verrà invocato, dovrà sapere la classe
o l’oggetto a cui appartiene
Mdescr = Idlist * Blocco * ( Loc | Id )
parametri formali
corpo del metodo
nome di classe
puntatore a oggetto
10
Operazioni sugli ambienti di metodi
e di classi
 cbind((r:Cenv), (i:Id), (c:Cdescr)) estende r
associando ad i il valore c
 cdefined(r:Cenv, i:Id) dice se r è definita per i
 mbind((m:Menv), (i:Id), (m:Mdescr)) estende m
associando ad i il valore m
 mdefined(m :Menv, i:Id) dice se m è definita per i
 instantiate((m:Menv), (l:Loc)) crea un nuovo
ambiente m1 diverso da m perché tutte le
descrizioni di metodi contengono l’oggetto l
11
La heap z
 z è una funzione da locazioni a descrizioni di
istanza (oggetto)
– z : Heap
– Heap = Loc -> Odescr
 cos’è una descrizione di oggetto?
Odescr = Id * Frame * Menv
classe
variabili di istanza
metodi di istanza
12
Operazioni sullo heap
 newheap() genera una heap vuota
 newloc(z) genera una nuova locazione in z
 hbind((z:Heap), (l:Loc), (o:Odescr)) estende z
associando ad l il valore o
 un oggetto viene creato con l’espressione new Id
–
–
–
–
genera il valore o:Odescr a partire dalla classe Id
l = newloc(z)
hbind((z:Heap), (l:Loc), (o:Odescr))
restituisce l
13
La pila di attivazioni s
 s è una pila di records di attivazione di metodi
– s : Astack
– Astack = Stack (Record)
 il record di attivazione
– oggetto o classe a cui il metodo appartiene
– pila di frames (blocchi annidati)
Record = ( Id | Loc ) * Stack(Frame)
classe
oggetto
variabili locali
14
Operazioni sulle pile (record, frame)
 emptystack() genera una pila vuota
 top((p:Stack(x)) restituisce l’elemento di tipo x in
testa a p
 pop((p:Stack(x)) modifica p eliminando
l’elemento in testa
 push((p:Stack(x),(e:x)) modifica p inserendo
l’elemento e in testa
 empty((p:Stack(x)) verifica se p è vuota
15
Le strutture dello stato (riepilogo 1)
 Ambiente delle classi
Cenv = Id -> Cdescr
Cdescr = Id * Frame * Menv * Frame* Menv
– cbind((r:Cenv), (i:Id), (c:Cdescr))
– cdefined((r:Cenv),(i:Id))
 Heap
Heap = Loc -> Odescr
Odescr = Id * Frame * Menv
– newheap()
– newloc ((z:Heap))
– hbind((z:Heap), (l:Loc), (o:Odescr))
16
Le strutture dello stato (riepilogo 2)
 Pila delle attivazioni
Astack = Stack (Record)
Record = ( Id | Loc ) * Stack(Frame)
– operazioni delle pile
17
Le strutture (ausiliarie) dello stato
(riepilogo 3)
 Ambiente dei metodi
Menv = Id -> Mdescr
Mdescr = Idlist * Blocco * ( Loc | Id )
– mbind((m:Menv), (i:Id), (m:Mdescr))
– mdefined ((m:Menv), (i:Id))
– instantiate((m:Menv), (l: Loc))
 Frames
Frame = Id -> Val
Val = (Bool | Int | Loc)
– newframe()
– bind((j:Frame) , (i:Id), (v:Val))
– update((j:Frame) , (i:Id), (v:Val))
– defined((j:Frame), (i:Id))
18
Uno stato (1)
puntatore ad oggetto
codice blocco f1
codice blocco f2
codice blocco f3
C
A
a 23
f1 (y,z)
C
b
c 5
f2 (w)
C
d ?
e ?
f3 ()
f4 (x)
?
?
C ()
?
codice blocco f4
codice blocco C
B
A
Object
 parte statica (classi)
19
Uno stato (2)
x
d 3
e
C
f3 ()
f4 (x)
C ()
stack
heap
puntatori al codice dei metodi
 parte dinamica (pila e heap)
– è in esecuzione il metodo f4 di una istanza di C
20
Cosa si “vede” in questo stato
x
d 3
e
C
f3 ()
f4 (x)
C ()
stack
heap
puntatori al codice dei metodi
 tutti i nomi delle classi
– attraverso queste, le variabili ed i metodi statici
21
Cosa si “vede” in questo stato
x
d 3
e
C
f3 ()
f4 (x)
C ()
stack
heap
 nomi di variabili (nell’ordine)
puntatori al codice dei metodi
– stack locale
– frame dell’oggetto a cui appartiene il metodo
– frames (statici) lungo la catena di sottoclassi
22
Cosa si “vede” in questo stato
x
d 3
e
C
f3 ()
f4 (x)
C ()
stack
heap
 nomi di metodi (nell’ordine)
puntatori al codice dei metodi
– ambiente di metodi dell’oggetto a cui appartiene il metodo
• lui incluso (ricorsione)
– ambienti di metodi (statici) lungo la catena di sottoclassi
23