Denotational Semantics October 26,2018 4口8，+三，+至+至a0 Denotational Semantics
Denotational Semantics October 26, 2018 Denotational Semantics
Syntax of the Imp Language (intexp)e::=0 11 1... x I -e l e+e l e-e 1... (boolexp)b::=true false I e-e l e<ele<el... b bAb l bvb l .. no quantified terms (comm)c::=x:=e I skip I cjc if b then c else c I while b do c 4口84三，4无+3月a0 Denotational Semantics
Syntax of the Imp Language (intexp) e ::= 0 | 1 | . . . | x | -e | e+e | e-e | . . . (boolexp) b ::= true | false | e=e | e < e | e < e | . . . | ¬b | b ∧ b | b ∨ b | . . . no quantified terms (comm) c ::= x := e | skip | c;c | if b then c else c | while b do c Denotational Semantics
Denotational Semantics -lintexp∈intexp→∑→Z Σevar→z I-boolexp∈boolexp→∑→B -lcomm E comm→∑→∑1 Σ.鸣ΣU山 x =ellcomm o=x ellintexp or] lx :=x 6llcomm ((x.7) =(X,7)Hx(【x*61meo(x,7) =1(X,7)1x42 =1(X42) IIskipllcamm lc;c.lcomm o if I[cllcomm=L (lic'lcommclcomm)otherwise Denotational Semantics
Denotational Semantics ~−intexp ∈ intexp → Σ → Z Σ def = var → Z ~−boolexp ∈ boolexp → Σ → B ~−comm ∈ comm → Σ → Σ⊥ Σ⊥ def = Σ ∪ {⊥} ~x := ecomm σ = σ{x { ~eintexp σ} ~x := x ∗ 6comm {(x, 7)} = {(x, 7)}{x { (~x ∗ 6intexp{(x, 7)})} = {(x, 7)}{x { 42} = {(x, 42)} ~skipcomm σ = σ ~c;c 0 comm σ = ( ⊥ if ~ccomm σ = ⊥ (~c 0 comm ◦ ~ccomm) σ otherwise Denotational Semantics
Denotational Semantics -lintexp∈intexp→∑→Z Σevar→z I-lboolexp∈boolexp→∑→B -lcomm E comm-→∑→∑1 Σ.ΣU山 Ix :=ellcomm=x ellintexp} Ix :=x *6llcomm((x,7)) =((x,7)Hx(Ix 6lintexp((x.7)])} ={(x,7){x42} ={(x,42)} Ilskip llcomm c= IIcic'llcamm if lclcomm c=L =(lc'llconmccomm)cr otherwise Denotational Semantics
Denotational Semantics ~−intexp ∈ intexp → Σ → Z Σ def = var → Z ~−boolexp ∈ boolexp → Σ → B ~−comm ∈ comm → Σ → Σ⊥ Σ⊥ def = Σ ∪ {⊥} ~x := ecomm σ = σ{x { ~eintexp σ} ~x := x ∗ 6comm {(x, 7)} = {(x, 7)}{x { (~x ∗ 6intexp{(x, 7)})} = {(x, 7)}{x { 42} = {(x, 42)} ~skipcomm σ = σ ~c;c 0 comm σ = ( ⊥ if ~ccomm σ = ⊥ (~c 0 comm ◦ ~ccomm) σ otherwise Denotational Semantics
Denotational Semantics -lintexp∈intexp→∑→Z Σ№var→z I-boolexp∈boolexp→∑→B -lcomm∈comm→∑→∑1 Σ.粤ΣU山 Ix :ellcomm =x [ellintexp [Ix :=x *6llcomm((x,7)} ={(x,7)Mx→(x*6 intexp(x,7)》 ={(x,7)Hx42} ={(x,42)》 [skiplcomm if I[cllcomm=L cic comm= (IIc'llcomm ollcllcomm)r otherwise Denotational Semantics
Denotational Semantics ~−intexp ∈ intexp → Σ → Z Σ def = var → Z ~−boolexp ∈ boolexp → Σ → B ~−comm ∈ comm → Σ → Σ⊥ Σ⊥ def = Σ ∪ {⊥} ~x := ecomm σ = σ{x { ~eintexp σ} ~x := x ∗ 6comm {(x, 7)} = {(x, 7)}{x { (~x ∗ 6intexp{(x, 7)})} = {(x, 7)}{x { 42} = {(x, 42)} ~skipcomm σ = σ ~c;c 0 comm σ = ( ⊥ if ~ccomm σ = ⊥ (~c 0 comm ◦ ~ccomm) σ otherwise Denotational Semantics