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