# 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

```