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 Main Program and Error values

Syntactic Categories

  I in Ident  (identifiers)
  E in Exp    (expressions)
  P in Prog   (full programs)

   E  ::=  0 | 1 | I | (E1 + E2) | (E1 / E2) 
        |  if E1 then E2 else E3 
        |  let I = E1 in E2 end
   P  ::=  program (I) ; E end .

          Int = { ..., -2, -1, 0, 1, 2, ... }   (integers)
   rho in Env = Ident --> Int U {undef}         (environments)

   EE : Exp --> Env --> Int U {err}
   PP : Prog --> Int --> Int U {err}

   EE [0] rho  =  0
   EE [1] rho  =  1

   EE [I] rho  =  ite(isInt(rho(I)), rho(I), err)

   EE [E1 + E2] rho =
     let n = EE [E1] rho ;  
         n' = EE [E2] rho
     in  ite(isInt(n) and isInt(n'), plus(n,n'), err)
     end

   EE [E1 / E2] rho =
     let n = EE [E1] rho ;  
         n' = EE [E2] rho
     in  if isInt(n) andalso isInt(n') andalso n' != 0
            then div(n,n') else err 
     end

   EE [ if E1 then E2 else E3 ] rho =
     let n = EE [E1] rho   
     in  if isInt(n) 
           then if n=0 then EE [E2] rho else EE [E3] rho
           else err
     end

   EE [[ let I = E1 in E2 end ]] rho  =  
     let n = EE [E1] rho   
     in  if isInt(n) then EE [[ E2 ]] rho[I |-> n] 
                     else err
     end

   PP [[ program (I); E end. ]] n =
     let fun rho(J) = undef
     in  EE [[ E ]] rho[I |-> n]
     end