Zadanie 2. Napisz semantykę denotacyjną w stylu kontynuacyjnym dla języka o następującej gramatyce:
Num3 n ::= . . . −1 | 0 | 1 | . . . Var3 x ::= x1 | x2 | . . . VarF3 f ::= f1 | f2 | . . .
Expr 3 e ::= n | x | e1+ e2 | e1− e2 | call f (x)
Dec 3 d ::= int x := e | d1; d2 | func f (x){I1 completing with I2} Instr 3 I ::= x := e | I1; I2 | skip | if e = 0 then I1 else I2 |
begin d; I end | return e W języku tym niestandardowe konstrukcje to
func f (x){I1 completing with I2} return e
Deklaracja func f (x){I1 completing with I2} powoduje wprowadzenie do środowiska pod identyfikator f funkcji, która wywoływana jest w semantyce przekazywania parametru przez zmienną oraz widoczności statycznej. Niestandardowość tego elementu polega na tym, że po każdym wykonaniu instrukcji return e w I1 wartość wyrażenia e jest zapamiętywana, a sterowanie przechodzi do wykonania instrukcji I2. Po zakończeniu wykonywania I2 następuje wyjście z funkcji f z zapamiętaną wartością wyrażenia e. Natomiast instrukcja return e w instrukcji I2 powoduje zmianę zapamiętanej wartości wyrażenia, ale nie powoduje przeskoku na początek I2, za to wykonanie przebiega normalnie dalej. Brak wykonania return e w I1 działa tak, jakby zapamiętana została domyślna wartość wyjściowa funkcji równa 0, zaś przejście do I2 następuje po wyczerpaniu instrukcji w I1.
Znaczenie pozostałych konstrukcji jest standardowe przy czym ewaluacja wyrażeń nastę- puje w naturalnej kolejności od lewej do prawej. Należy założyć, że identyfikatory zmiennych i funkcji pochodzą z rozłącznych zbiorów (tzn.Var∩VarF= ∅). Trzeba podać typy oraz definicje funkcji denotujących dla wyrażeń, instrukcji oraz deklaracji. Należy też podać określenie wszystkich dziedzin semantycznych, z których korzysta się przy podawaniu semantyki. Jeśli trzeba, można wykorzystać funkcję alloc odpowiedniego typu (ten typ należy podać), która określać będzie dotychczas niewykorzystywaną lokację.
Przykład:
01: begin
02: int x := 0;
03: func f(y) { 04: begin
05: if x = 0 then
06: begin
07: int z := x+y+1;
08: return z
09: end
10: else
11: return y - 1 12: end
13: completing with 14: y := x+y 15: };
16: x := call f(x);
17: x := call f(x) + x 18: end
W wyniku działania tego programu wartością zmiennej x tuż przed wyjściem z bloku w wierszu 18. będzie 2. Wy- konanie kodu wygląda tak: najpierw następuje inicjaliza- cja x na 0. Następnie zmiennej x nadawana jest war- tość wynikająca z wywołania call f (x). Wywołanie to w swoim kodzie sprawdza najpierw, że zmienna x jest równa 0 i przechodzi do pierwszej gałęzi instrukcji if.
Tam zapamiętywana jest jako wartość wyjścia z funkcji liczba 1, po czym sterowanie przechodzi do instrukcji za completing with w linii 13. Tam ustalana jest wartość zmiennej y na 0. Zarazem, w wyniku wołania przez zmi- enną, na 0 ustawiana jest wartość zmiennej x. Tu następuje wyjście z funkcji z wartością 1. Zatem x w linii 16.
otrzyma wartość 1. Przechodzimy do wywołania f w linii 17. Tym razem if w treści funkcji przeniesie sterowanie do wiersza 11. (x jest 1), gdzie zostanie zapamiętana wartość wynikowa 0. Następnie w instrukcji w wierszu 14. nastąpi przypisanie 2 na y. Następnie sterowanie wyjdzie z funkcji, by dokończyć przypisanie w wierszu 17. Tam na x przypisana zostanie wartość wynikowa 0 funkcji powiększona o wartość zmiennej x, czyli 2. W wyniku x otrzyma zapowiadaną wartość 2.
Rozwiązanie:
Dziedziny Podstawowe dziedziny semantyczne mają tutaj następującą postać:
• Val= Z⊥,
• State=Loc→Val,
Określimy dwa rodzaje środowisk:
Env= Var→Loc⊥
EnvF= VarF→Func
gdzie Func jest zdefiniowane dalej. W intencji pierwsze środowisko służy do przechowywania informacji o zwykłych zmiennych, zaś drugie do przechowywania informacji o funkcjach.
Funkcja alloc ma następujący typ: alloc :State→State×Loc.
Typy kontynuacji wyglądają w następujący sposób:
• Cont=State→State,
• ECont=Val→Cont,
• DCont=Env→EnvF→Cont,
• Func=Loc→ECont→Cont,
• RHan=Val→Cont→Cont,
gdzie RHan jest typem, którego wartości będą wspomagać obsługę konstrukcji return.
Typy funkcji denotujących
• E :Expr → Env → EnvF → ECont → Cont,
• D :Dec → Env → EnvF → DCont → Cont,
• I :Instr → Env → EnvF → RHan → Cont → Cont.
Denotacja dla programów Zakładamy, że dla programu, który składa się z instrukcji I denotacją jest IJI K ρ ρfκhκ0s0 gdzie ρ = λx ∈Var.⊥, ρf = λx ∈VarF.⊥, κh= λv ∈Val.λκ ∈ Cont.κ, κ0= λs ∈State.s, s0 = λl ∈Loc.⊥.
Denotacja wyrażeń
• EJnK = λρ ∈Env.λρf ∈EnvF.λκ ∈ECont.κn
• EJxK = λρ ∈Env.λρf ∈EnvF.λκ ∈ECont.λs ∈State.κ(s(ρx))s
• EJe1+ e2K = λρ ∈Env.λρf ∈EnvF.λκ ∈ECont.
EJe1Kρρf(λn1∈Val.EJe2Kρρf(λn2 ∈Val.κ(n1+ n2)))
• EJe1− e2K = λρ ∈Env.λρf ∈EnvF.λκ ∈ECont.
EJe1Kρρf(λn1∈Val.EJe2Kρρf(λn2 ∈Val.κ(n1− n2)))
• EJcall f (x)K = λρ ∈Env.λρf ∈EnvF.λκ ∈ECont.ρff (ρx)κ
Denotacja deklaracji
• DJint x := eK = λρ ∈Env.λρf ∈EnvF.λκ ∈DCont.λs ∈State.
EJeK ρ ρf(λn ∈Val.λs0 ∈State.κ ρ[x 7→ l] ρfs00[l 7→ v])s where (s00, l) = alloc(s0)
• DJd1; d2K = λρ ∈Env.λρf ∈EnvF.λκ ∈DCont.
DJd1K ρ ρf(λρ0 ∈Env.λρ0f ∈EnvF.DJd2K ρ
0ρ0f(λρ00∈Env.λρ00f ∈EnvF.κ ρ00ρ00f))
• DJfunc f (x){I1 completing with I2}K = λρ ∈Env.λρf ∈EnvF.λκ ∈DCont.
κ ρ ρf[f 7→ fixF ] where
– F = λφ ∈Func.λl ∈Loc.λκ ∈ECont.λs ∈State.
IJI1Kρ[x 7→ l]ρf[f 7→ φ]σ1κ1s0[l0 7→ 0]
where
∗ (s0, l0) = alloc(s)
∗ κ1 = IJI2Kρ[x 7→ l]ρf[f 7→ φ]σ2κ2
∗ σ1 = λv ∈Val.λκ00∈Cont.λs00 ∈State.κ1s00[l0 7→ v]
(zapamiętujemy wartość v jako wartość do wyjścia z funkcji i skaczemy do I2),
∗ κ2 = λˆs ∈State.κ(ˆsl0)ˆs
∗ σ2 = λv ∈Val.λκ00∈Cont.λs00∈State.κ00s00[l0 7→ v] (zapamiętujemy wartość v jako wartość do wyjścia z funkcji i kontynujemy wykonanie po return).
Denotacja instrukcji
• IJx := eK = λρ ∈Env.λρf ∈EnvF.λσ ∈RHan.λκ ∈Cont.
EJeK ρ ρf(λn ∈Val.λs0∈State.κ s0[ρx 7→ n])
• IJI1; I2K = λρ ∈Env.λρf ∈EnvF.λσ ∈RHan.λκ ∈Cont.IJI1K ρ ρf(IJI2K ρ ρfκ)
• IJskipK = λρ ∈Env.λρf ∈EnvF.λσ ∈RHan.λκ ∈Cont.κ
• IJif e = 0 then I1 else I2K = λρ ∈Env.λρf ∈EnvF.λσ ∈RHan.λκ ∈Cont.
EJeK ρ ρf(λn ∈Val.ifte(n =Val 0, IJI1K, I JI2K) ρ ρfσκ)
• IJbegin d; I endK = λρ ∈Env.λρf ∈EnvF.λσ ∈RHan.λκ ∈Cont.
DJdK ρ ρf(λρ0∈Env.λρ0f ∈EnvF.IJI K ρ
0ρ0fσ κ)
• IJreturn eK = λρ ∈Env.λρf ∈EnvF.λσ ∈RHan.λκ ∈Cont.
EJeKρ ρf(λv ∈Val.σvκ)
