# Denotational Semantics

### Example: language with combined expressions and commands

**Now we complicate things even more...**

In this language, evaluation of expressions may have side effects...
i.e., they may change the state. We must now give some structure to
states.
**Syntactic Categories**

I in Ident (identifiers)
L in Lexp (l-expressions, or references)
E in Exp (expressions, commands)
P in Prog (full programs)

**Syntax BNF**
L ::= I
E ::= 0 | 1 | I | !L | E1; E2 | (E1 + E2)
| let I = E1 in E2 end
| new I := E1 in E2 end
| L := E
| if E1 then E2 else E3
| while E1 do E2
P ::= program (I) ; E end .

**Value Domains**
n in Int = { ..., -2, -1, 0, 1, 2, ... } (integers)
alpha in Loc (no structure details...)
sigma in States = Loc --> Int U {unused} (states, of memory)
rho in Env = Ident --> Int U Loc U {undef}

**Semantic Functions**
LL : Lexp --> Env --> States --> Loc
MM : Exp --> Env --> States --> (Int * States)
PP : Prog --> Int --> Int

**Semantic Equations**
LL [ I ] rho sigma = rho(I)
PP [ program (I); E end. ] n =
let fun rho(J) = undef
fun sigma(alpha') = unused
alpha be some Loc such that sigma(alpha) = unused
(v,sigmaF) = MM [[ E ]] rho[I |-> alpha] sigma[alpha |-> n]
in sigmaF(alpha)
end
MM [ 0 ] rho sigma = (0,sigma)
MM [ 1 ] rho sigma = (1,sigma)
MM [ I ] rho sigma = (rho(I),sigma)
MM [ !L ] rho sigma =
let alpha = LL [ L ] rho sigma
in (sigma(alpha),sigma)
end
MM [ E1 + E2 ] rho sigma =
let (n,sigma') = MM [E1] rho sigma
(m,sigma") = MM [E2] rho sigma'
in (plus(n,m),sigma")
end
MM [ if E1 then E2 else E3 ] rho sigma =
let (n,sigma') = MM [E1] rho sigma
in ite(n=0, MM [E2] rho sigma', MM [E3] rho sigma' )
end
MM [ E1; E2 ] rho sigma =
let (n,sigma') = MM [E1] rho sigma
in MM [E2] rho sigma'
end
(* note that n, the value of E1, is discarded *)
MM [[ while E1 do E2 ]] rho sigma =
let fun p(sigma') =
let (b,sigma") = MM [E1] rho sigma'
(m,sigma''') = MM [E2] rho sigma"
in ite(b=0, p(sigma'") else (b,sigma") )
end
in p(sigma)
end
MM [ let I=E1 in E2 end ] rho sigma =
let (n,sigma') = MM [E1] rho sigma
rho' = rho[I |-> n]
in MM [E2] rho' sigma'
end
MM [ L := E ] rho sigma =
let alpha = LL [ L ] rho sigma
(n,sigma') = MM [E] rho sigma
in (n,sigma'[alpha |-> n])
end
MM [ new I := E1 in E2 end ] rho sigma =
let (n,sigma') = MM [E1] rho sigma
alpha be some Loc such that sigma'(alpha) = unused
in MM [E2] rho[I |-> alpha] sigma'[alpha |-> n]
end