Denotational Semantics

Overview and example
Language of Propositional Logic
Language of Simple Expressions
Language Main Program and Error Values
Language with State (Imperative)
Language with Combined Expressions and Commands
Language with Function Calls

Example: language with State (imperative)

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)

   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 .

       n in Int = { ..., -2, -1, 0, 1, 2, ... }   (integers)
   sigma in States                                (states, of memory)

   EE : Exp --> ???
   CC : Comm --> States --> States
   PP : Prog --> Int --> Int 

   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'
      end

      (* 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)  
     end