Napisz semantykę denotacyjną programów dla języka o następującej gramatyce: N um 3 n

Zadanie 2. Napisz semantykę denotacyjną programów dla języka o następującej gramatyce:

N um 3 n ::= . . . −1 | 0 | 1 | . . . Var3 x ::= x1 | x₂ | . . . VarP3 p ::= p₁ | p₂ | . . . Expr 3 E ::= n | x | E₁+ E₂

Dec 3 D ::= int x := E | D1; D2 | proc p(x){I}

Instr 3 I ::= x := E | cbv | cbr | cio | I₁; I₂ | skip |

if E = 0 then I1 else I2 | call p(x) | begin D; I end

W języku tym niestandardowymi konstrukcjami są instrukcje cbv, cbr oraz cio. Dzię- ki nim możliwe jest dynamiczne zmienianie trybu wywoływania procedur. Wykonanie cbv powoduje włączenie trybu wołania przez wartość, w tym trybie każde wywołanie call p(x) będzie powodowało wykonanie ciała procedury p tak, że odwołania do zmiennych są w seman- tyce wołania przez wartość. Podobnie wykonanie cbr włącza tryb wołania przez zmienną, a cio włącza tryb wołania typu in-out. Wołanie przez wartość i zmienną są rozumiane stan- dardowo. Wołanie typu in-out to takie wołanie, w którym w momencie wywołania procedury rezerwowane jest miejsce na nową zmienną, na którą przepisywany jest parametr aktualny.

Następnie wszystkie opracje na parametrze formalnym wykonywane są na tej świeżo zarez- erwowanej zmiennej. W momencie wyjścia z procedury wartość tej zmiennej jest z kolei przepisywana na zmienną, bedącą parametrem aktualnym.

Początkowo program znajduje się w trybie wołania przez wartość. Wymagamy, aby widocz- ność identyfikatorów w procedurach była statyczna, ale procedury mają być rekurencyjne.

Należy założyć, że identyfikatory zmiennych i procedur pochodzą z rozłącznych zbiorów (tzn. Var ∩VarP = ∅). Trzeba podać typy i definicje funkcji denotujących dla wyrażeń, deklaracji oraz instrukcji. Należy też podać określenie wszystkich dziedzin semantycznych, z których korzysta się przy określaniu semantyki. Jeśli trzeba, można wykorzystać funkcję alloc odpowiedniego typu (ten typ należy podać), która określać będzie dotychczas niewyko- rzystywaną lokację.

Przykład:

1: begin

2: int y := 3;

3: proc p(x) { 4: x := x + y 5: };

6: proc q(x) { 7: x := x + 1;

8: cio;

9: call p(x);

10: cbv;

11: x := x + 2;

12: x := x + x;

13: call p(x);

14: };

15: cbr;

16: call q(y);

17: call p(y) 18: end

W wyniku działania tego programu wartością zmiennej y tuż przed wyjściem z bloku w wierszu 18. będzie 20. Jego wykonanie wygląda tak: po inicjalizacji y na 3 następuje w wierszu 15. zmiana trybu na tryb wołania przez zmienną i wywołanie w tym trybie procedury q. W ten sposób we wnętrzu tej procedury staje się dostępna pod nazwą x zmienna globalna y i ma ona wartość 3. Następnie zmienna ta jest zwiększana do 4 (jednocześnie zmienia się na 4 wartość y)

i następuje w wierszu 8. przełączenie trybu na tryb typu in-out. W tym momencie wywołanie call p(x) w wierszu 9. powoduje utworzenie we wnętrzu procedury p nowej zmiennej x i przepisanie do niej wartości dotychczasowej zmiennej x, czyli 4. Po wykonaniu przypisania z wiersza 4. zmienna x ma wartość 8. Ta wartość przy powrocie z p jest przenoszona do zmiennej x wewnątrz q, co skutkuje jednoczesnym przypisaniem 8 na tę zmienną oraz na zmienną globalną y. Dalej następuje zmiana trybu na tryb wołania przez wartość oraz dwa przypisania, które nadają zmiennym x i y wartość 20. Wykonane następnie wywołanie call p(x) nie zmienia wartości zmiennych x i y, gdyż w ciele tej procedury jedynie przypisuje się na zmienną lokalną, co przy semantyce wołania przez wartość nie wpływa na zmienne zadeklarowane poza tą procedurą. W następnym kroku wychodzimy z procedury q i wracamy do głównego bloku, gdzie wywołujemy call p(y) we wciąż obowiązującym trybie wołania przez wartość.

Wywołanie to, jak wspomnieliśmy wcześniej, niczego nie zmienia, zatem zmienna y po wyjściu z tej procedury, a co za tym idzie na końcu bloku, ma zapowiedzianą wartość 20.

Rozwiązanie:

Przedstawimy semantykę denotacyjną w stylu bezpośrednim. Semantyka kontynuacyjna nie jest potrzebna, bo nie ma w zadaniu nielokalnych skoków.

Dziedziny Podstawowe dziedziny semantyczne mają tutaj następującą postać:

• Val= Z⊥,

• Loc jest abstrakcyjnym zbiorem lokacji, takim że ⊥ ∈Loc,

• Store=Loc→Val,

• CKind= {cbv, cbr, cio}

• State=Store×CKind,

• Env= {f₁∪ f₂| f₁ ∈Var→Loc, f₂∈VarP→Proc}.

Wprowadzenie znaczników cbv, cbr, cio pozwala na kontrolowanie działania fraz języka postaci cbv, cbr i cio, które związane są z rodzajem wołania.

Dodatkowo wprowadzamy dziedzinę

Proc=Loc→State→State,

służącą do reprezentacji procedur. Funkcja alloc ma następujący typ: alloc :Store→Store× Loc. Dla uproszczenia zapisu wprowadzamy notację: Niech s = (s, k) ∈ State, p ∈Proc, and l ∈Loc. Przeładowując notację, definiujemy s[x 7→ l] = (s[x 7→ l], k) i s[p 7→ p] = (s[p 7→ p], k).

Przez π₁, π2 oznaczamy rzutowania na odpowiednio pierwszą i drugą współrzędną pary.

Typy funkcji denotujących

• E : Expr →Env→Store→Val,

• I : Instr →Env→State→State,

• D : Dec →Env→State→Env×State.

Denotacja dla programów Zakładamy, że dla programu, który składa się z instrukcji I denotacją jest IJI Kρ⁰s0, gdzie ρ₀x = ⊥ dla x ∈Var∪VarP, s0x = ⊥ dla x ∈Loc.

W poniższej semantyce dla uproszczenia pomijamy sprawdzanie, czy funkcja jest określona przed jej zastosowaniem oraz sprawdzanie, czy argument środowiska jest z odpowiedniego zbioru zmiennych.

Denotacja wyrażeń

• EJnK = λρ ∈Env.λs ∈Store.n,

• EJxK = λρ ∈Env.λs ∈Store.s(ρx)),

• EJE1+ E₂K = λρ ∈Env.λs ∈Store.EJE1Kρs + E JE2Kρs,

Denotacja instrukcji

• IJx := E K = λρ ∈Env.λs ∈State.s[(ρx) 7→ EJE K ρ s],

• IJcbvK = λρ ∈Env.λs ∈State.(π1s, cbv),

• IJcbrK = λρ ∈Env.λs ∈State.(π1s, cbr),

• IJcioK = λρ ∈Env.λs ∈State.(π₁s, cio),

• IJI1; I₂K = λρ ∈Env.(IJI2Kρ) ◦ (I JI1Kρ),

• IJskipK = λρ ∈Env.λs ∈State.s,

• IJif E = 0 then I1 else I2K = λρ ∈Env.λs ∈State.

ifte(EJE Kρ(π1s) = 0, IJI1Kρs, I JI2Kρs),

• IJcall p(x)K = λρ ∈Env.λs ∈State.ρp(ρx)s,

• IJbegin D; I endK = λρ ∈Env.λs ∈State.let (ρ⁰, s⁰) = DJDKρs in I JI Kρ

0s⁰. Denotacja deklaracji

• DJint x := E K = λρ ∈Env.λs ∈State.let v = EJE K ρ s in let (s⁰, l) = alloc(π1s) in (ρ[x 7→ l], (s⁰[l 7→ v], π2s)),

• DJD1; D2K = λρ ∈Env.λs ∈State.let (ρ⁰, s⁰) = DJD1K ρ s in DJD2K ρ

0s⁰,

• DJproc p(x){I }K = λρ ∈Env.λs ∈State.(ρ[p 7→ fixF ], s) where F = λϕ ∈Proc.λl ∈Loc.λs ∈State.let s⁰⁰= IJI K ρ

0s⁰in ifte(π₂s = cio, s⁰⁰[l 7→ π₁s⁰⁰l₂], s⁰⁰)

where

ρ⁰ = ρ[x 7→ l2][p 7→ ϕ]

s⁰ = (s2, π2s) where

(s₂, l₂) = ifte(π₂s = cbr, (π₁s, l), (s₁[l₁ 7→ π₁s l], l₁)) where

(s₁, l₁) = alloc(π₁s).