1

Semantica Operazionale di un frammento di Java:

le regole di transizione

estensione (con piccole varianti) di quella in

Barbuti, Mancarella, Turini,

Elementi di Semantica Operazionale,

appunti di Fondamenti di Programmazione

2

Regole di transizione

diverse relazioni di transizione, in corrispondenza dei diversi tipi di costrutti del linguaggio

– espressioni, comandi, dichiarazioni ecc.

k

3

Dichiarazione di classeClass_decl := class Id extendsextends Id {Static_var_decl_listStatic_var_decl_listStatic_meth_decl_listStatic_meth_decl_listInst_var_decl_listInst_meth_decl_listCostruttoreCostruttore }

assunzioni– c’è sempre extends

• ogni classe estende la classe Object

– le dichiarazioni di variabili e metodi statici sono “raggruppate”– esiste sempre il costruttore

4

Semantica informale delle classi

variabili e metodi statici appartengono alla classe variabili e metodi di istanza appartengono agli

oggetti (istanze della classe) una classe definisce un tipo (nome della classe)

– gli oggetti della classe hanno quel tipo

relazioni di sottoclasse ed ereditarietà – gerarchia di tipi, realizzata con extends– la radice della gerarchia è la classe predefinita Object

5

Ereditarietà

se cdown è una sottoclasse (estende) cup

– variabili e metodi statici di cup (e delle sue superclassi) sono visibili direttamente da cdown

– variabili e metodi di istanza di cup (e delle sue superclassi) diventano anhe variabili e metodi di istanza degli oggetti di cdown

– Tipo degli oggetti di cup è anche tipo degli oggetti di cdown

a meno di overriding

6

Overriding

se cdown è una sottoclasse (estende) cup

– un metodo di istanza di cup (e delle sue superclassi) può essere ridefinito (stesso nome e tipi) in cdown

– l’idea è quella di definire un metodo più specializzato, che rimpiazza quello definito in una delle superclassi

l’overriding non “dovrebbe” essere possibile per le variabili e per i metodi statici

– ma questo non è sempre garantito dal compilatore– comportamenti complessi e poco prevedibili– assumeremo che non si verifichi mai

7

Inizializzazioni

Java permette di inizializzare (al valore di una espressione) sia le variabili statiche che quelle di istanza in una dichiarazione

– le inizializzazioni delle variabili statiche vengono effettuate la prima volta

che si usa una classe– le inizializzazioni delle variabili di istanza vengono effettuate all’atto

della creazione di una istanza (oggetto)

per semplicità, decidiamo di non avere inizializzazioninon avere inizializzazioni nelle dichiarazioni di variabile all’interno di classi

Le inizializzazioni possono essere affidatepossono essere affidate al(i) costruttore(i)– eseguito quando si crea un’istanza

8

Il costruttore

i costruttori sono usati per la creazione di un oggetto:– Inizializzazione dello stato (variabili di istanza)

anche per i costruttori esiste un meccanismo di ereditarietà

se c è una classe che ha come superclassi (nell’ordine) le classi c1, c2,…, cnObject, – all’atto della creazione di una istanza di c– si eseguono (nell’ordine) i costruttori di cn,…,c2,c1,c

9

Dichiarazione di classe

Class_decl := class Id extends Id {Static_var_decl_listStatic_meth_decl_listInst_var_decl_listInst_meth_decl_listCostruttore }

Cenv = Id -> Cdescr

Cdescr = Id * Frame * Menv * Frame* Menv la relazione di transizione

Class_decl * Cenv cdeclcdecl Cenv

10

Dichiarazione di classe

Cenv = Id -> Cdescr

Cdescr = Id * Frame * Menv * Frame* Menv

Class_decl * Cenv cdecl Cenv

(b) = (_,_,_, b, b) b(b) = (_, cb, _)<svdl, newframe()> vdecl <ivdl, copy(b)> vdecl a

<smdl, a, memptyenv()> mdecl <imdl, a, b> mdecl a________________________________________________<<classclass a a extendsextends b {svdl smdl ivdl imdl c}, b {svdl smdl ivdl imdl c}, > > cdeclcdecl cbind(cbind(, a, (b, , a, (b, , , , , aa, mbind(, mbind(aa, a, ([], c, a, ([], cbb c, a)))) c, a))))

11

Dichiarazioni di metodi

Method_decl := Id (Idlist) Blocco

guardiamo solo la dichiarazione singola– per una lista di dichiarazioni, si ripete a partire dal

risultato precedente

Menv = Id -> Mdescr

Mdescr = Idlist * Blocco * ( Loc | Id ) la relazione di transizione

Method_decl * Id * Menv mdeclmdecl Menv

12

Dichiarazione di metodo

Method_decl := Id (Idlist) Blocco

<m (idlist) blocco, c, <m (idlist) blocco, c, >> mdeclmdecl mbind(mbind(, m, (idlist, blocco, c)), m, (idlist, blocco, c))

come già osservato, l’eventuale overriding è realizzato automaticamente da mbind

13

Dichiarazioni di variabili

Var_decl := Type Id; come già osservato, le dichiarazioni non hanno

inizializzazione guardiamo solo la dichiarazione singola

– per una lista di dichiarazioni, si ripete a partire dal risultato precedente

Frame = Id -> Val Val = (Bool | Int | Loc)

la relazione di transizione

Var_decl * Frame vdeclvdecl Frame

14

Dichiarazione di variabile

Frame = Id -> Val Val = (Bool | Int | Loc)Var_decl * Frame vdecl Frame

<t id , <t id , > > vdeclvdecl bind(bind(, id, default(t)), id, default(t))

come già osservato, non ci deve essere overriding– id non deve essere definito in

in realtà un Frame è una struttura modificabile– update modifica l’argomento

la funzione default genera un valore di tipo t– 0 se t è intero– null se t è il tipo di un oggetto