Denotational Semantics

Example: language with State (imperative)

Now we complicate things even more...
Previous languages have been functional. Functional semantics sure work well for functional languages. Nothing messy and non-function-like.

In imperative languages we have a program state... variable that can store values and have then changed.

We will need some structure in the denotational definition to deal with this... like we added the Env environments earlier to handle bindings of names to values.

We will leave out the error value stuff now that you've seen how it's done.

Syntactic Categories

  I in Ident  (identifiers)
  E in Exp    (expressions)
  C in Comm   (commands)
  P in Prog   (full programs)
Syntax BNF
   E  ::=  0 | 1 | I | (E1 + E2) | (E1 / E2) 
        |  let I = E1 in E2 end
   C  ::=  C1 ; C2
        |  if E then C1 else C2
        |  while E do C
   P  ::=  program (I) ; C end .
Value Domains
       n in Int = { ..., -2, -1, 0, 1, 2, ... }   (integers)
   sigma in States                                (states, of memory)
Semantic Functions
   EE : Exp --> ???
   CC : Comm --> States --> States
   PP : Prog --> Int --> Int 
Semantic Equations
   CC [ if E then C1 else C2 ] sigma =
      ite( isTrue(EE [E] sigma), CC [C1] sigma, CC [C2] sigma )
      (* we presume for now that EE knows how to use a state
         rather than an environment *)

   CC [ C1; C2 ] sigma =
      let sigma' = CC [C1] sigma 
      in  CC [C2] sigma'

      (* or, CC [C1; C2] = CC [C1] o CC [C2] in functionals *) 

   CC [[ while E do C ]] sigma =  
     let fun p(sigma') = 
            if isTrue(EE [E] sigma') then p(CC [C] sigma') else sigma'
     in  p(sigma)  

This last equation is recursive (remember loops in Mills'?)