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