Wejście - wyjście: semantyka denotacyjna

Rozszerzamy składni_{}e j_{}ezyka o wejście-wyjście:

Składnia

• e ::= m | v | (e + e′) | (e − e′) | (e ∗ e′) | \underline{read}

• b ::= t | b∨b′ | e = e′ | ¬b

• d ::= \underline{var} v | d_{1}; d_{2}

• c ::= \underline{skip} | v := e | c; c′ | \underline{if} b \underline{then} c \underline{else} c′ | \underline{while} b \underline{do} c | \underline{begin} d; c \underline{end} | \underline{write}(e)

Musimy zmodyfikować dziedziny semantyczne. Dotychczas mielismy S = [Loc → Sv + \{ \underline{wolna} \}] – stany (=pami_{}eć) Teraz rozszerzamy stany o wejście i wyjście. Mamy:

• V al = {N + B + {⊥}}

• In = V al^{∗}

• Out = V al^{∗} • pusty ci _{}ag wartości b_{}edziemy oznaczać ϵ

• S = M × In × Out

• M = [Loc → Sv + \{ \underline{wolna} \}] – stany (pami_{}eć) B_{}edziemy używać pomocniczych funkcji:

• hd : V al^{∗} → V al

• tl : V al^{∗} → V al∗ Funkcje semantyczne

A : Aexp → [Env → [S → N_{⊥} × In]] B : Bexp → [Env → [S → B_{⊥} × In]] D : Decl → [Env → [M → Env × M]] C : Com → [Env → [S → S_{⊥}]] Równania semantyczne

Aexp

A[[n]] = λρ ∈ Env.λs ∈ S.(n, (s)_{2})

A[[v]] = λρ ∈ Env.λ(m, i, o) ∈ S.if ρv ∉ Loc then ⊥ else if m(ρv) = ⊥_{N} then ⊥_{N} else (m(ρv), i)

A[[ \underline{read} ]] = λρ ∈ Env.λs ∈ S.if i = ϵ then ⊥ else (hd(i), tl(i))

A[[e_{0} + e_{1}]] = λρ ∈ Env.λ(m, i, o) ∈ S. let (w′, i′) = A[[e_{0}]]ρ(m, i, o) in if w′ = ⊥_{N} then ⊥ else let (w′′, i′′) = A[[e_{1}]]ρ(m, i′, o) in if w′′ = ⊥_{N} then ⊥ else (w′ + w′′, i′)

Pozostałe wyrażenia analogicznie.

Decl

D[[ \underline{var} v]] = λρ ∈ Env.λs ∈ S. (ρ[(new(s))_{1}/v], (new(s))_{2})

D[[d_{1}; d_{2}]] = λρ ∈ Env.λs ∈ S. D[[d_{2}]](D[[d_{1}]]ρs)_{1}(D[[d_{1}]]ρs)_{2}

Com

C[[\underline{skip}]] = λρ ∈ Env.λs ∈ S.s

C[[v := e]] = λρ ∈ Env.λ(m, i, o) ∈ S .if ρv ∉ Loc then ⊥_{S} else if (A[[e]]ρ(m, i, o))_{1} = ⊥_{N} then ⊥_{S} else (m[(A[[e]]ρ(m, i, o))_{1}/ρv], (A[[e]]ρ(m, i, o))_{2}, o)

C[[ \underline{write}(e) ]] = λρ ∈ Env.λ(m, i, o) ∈ S. let (w, i′) = A[[e]]ρ(m, i, o) in if w = ⊥_{N} then ⊥_{S} else (m, i′, w.o)

Pozostałe instrukcje analogicznie.