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 of propositional logic

  P in Prop  (propositions)
  F in Form  (formulae)

   F  ::=  P  |  ~ F  |  F ==> F

          Bool = { true, false }      boolean logic values
   rho in Assign = P --> Bool         truth assignments

   MM :  Form  --> Assign -->  Bool
     means MM mapps a formula and an assignment into a boolean value
     the assignment tells the truth values of atomic propositions

   MM [P] rho  =  rho(P) 
   MM [~F] rho  =  ~ MM [F] rho
   MM [F1 ==> F2] rho  =  ~ MM [F1] rho  v  MM [F2] rho