A.A. 2001-02

Linguaggi di Programmazione I: Paradigmi

Prova scritta del 23 gennaio 2002: soluzioni

Esercizio 1.

M ::= x | M.m(M_{1}, … M_{n})

Esercizio 2. La funzione d può essere vista come proditto della compilazione di un programma Java. A partire da questa funzione e dalla relazione ≤ di sottotipo, otteniamo una funzione

d^{†} : K × Ide × T^{∗} → (T ∪ ⊥)

definita come segue: d^{†}(C, m, < t_{1}, … t_{n} >) = t se e solo se esistono C′, t′_{1}, … t′_{n} tali che:

– d(C′, m, < t′_{1}, … t′_{n} >) = t;

– C ≤ C′ e t_{i} ≤ t′_{i} per i = 1 … n;

– per ogni C′′ e t′′_{1}, … t′′_{n}, se d(C′′, m, < t′′_{1}, … t′′_{n} >) ≠ ⊥ e C ≤ C′′ e t_{i} ≤ t′′_{i} per i = 1 … n, allora C′ ≤ C′′.

Indichiamo con Γ un generico contesto dei tipi, che associa tipi a variabili. Il sistema dei tipi per JExp è il seguente:

[var] Γ_{1}, x : t, Γ_{2} ⊢ x : t

[call] \frac{Γ ⊢ M : C Γ ⊢ M_{i} : t_{i}}{Γ ⊢ M.m(M_{1}, … M_{n}) : t} (se d^{†}(C, m, < t_{1}, … t_{n} >) = t)

Esercizio 3. Sia

E ∈ Env = Var ⟶^{fin} Obj,

dove Obj è un insieme {o_{1}, o_{2} … } di “oggetti” su cui si assume definita una funzione

class : Obj → K che restituisce la classe di ciascun oggetto. Assumiamo inoltre che sia data una funzione

frame : K × Ide × T^{∗} → (Var^{∗} × JExp) ∪ ⊥

che svolge a tempo di esecuzione un lavoro analogo a quello che d^{†} svolge a tempo di compilazione, restituendo il frame di attivazione di un metodo, ovvero il suo corpo e i suoi parametri formali.

La semantica operazionale di JExp è la relazione

⇝^{M}⊆ Env × JExp × Obj

definita dalle seguenti regole:

[var] E ⊢ x ⇝ o (se E(x) = o)

[call] \frac{E ⊢ M ⇝ o E ⊢ M_{i} ⇝ o_{i} \{(x_{i}, o_{i})\} ⊢ p ⇝^{p} o′}{E ⊢ M.m(M_{1}, … M_{n}) ⇝ o′} (∗)

(∗) se frame (C, m, < class(o_{1}), … class(o_{n}) >) = (< x_{1}, … x_{n} >, p)