Figure 2

and the


Note, the names  cc, ee and dd  are used for the ``valuation functions'' which are usually called C, E and D because the notation below is tending to a programming language.

       answer = empty + (value x answer)
     location = {1, 2, 3, ... }
  s:    store = location -> {value + undefined value + unbound}
  e:      env = ident -> location + prok
         prok = cont -> store -> answer
  c:     cont = store -> answer
 dc:    dcont = env -> store -> answer
  k:     kont = value -> store -> answer

 cc: statement -> env -> cont -> store -> answer

 ee: exp -> env -> kont -> store -> answer

 dd: dec -> env -> dcont -> store -> answer

 cc "begin <statement> end"  e  c  s  = cc "<statement>"  e  c  s

 cc "<s1>;<s2>;..."  e  c  s  =  cc "<s1>"  e  s2c  s
    where s2c = (store s)answer: cc "<s2>;..." e c s

 cc "<dec>;<s2>;..."  e  c  s  =  dd "<dec>"  e  statpart  s
    where statpart = (env e, store s)answer:
      cc "<s2>;..." e c s

 cc "if <exp> then <s1> else <s2>" e c s
   = ee "<exp>" e cond s
     where cond = (value v, store s)answer:
       if v=1 then cc "<s1>" e c s  else cc "<s2>" e c s

 cc "while <exp> do <statement>" e c s
   = ee "<exp>" e loop s
     where loop = (value v, store s)answer:
       if v=1 then cc "<statement>" e again s
         where again = (store s)answer:
           cc "while <exp> do <statement>" e c s

 cc "<ident> := <exp>" e c s  = ee "<exp>" e update s
   where update = (value v, store s)answer: c news
     where news=(location l)value:
       if l=e(<ident>) then v else s(l)

 cc "output <exp>"  e  c  s  =  ee "<exp>"  e  doio s
   where doio = (value v, store s)answer: (v, c(s))

 cc "<ident>"   e  c  s  =  e "<ident>" c s

 dd "var <ident1>,<ident2>,..." e dc s
   = dd "var <ident1>" e otherdecs s
     where otherdecs = (env e, store s)answer:
       dd "var <ident2>,..." e dc s

 dd "var <ident>"  e  dc  s  = dc newenv news
   where newenv=(identifier i) union(location,prok):
     if i="<ident>" then new(s) else e(i)
   and  news =(location l)value:
     if l=new(s) then undefined value else s(l)

 dd "proc <ident>=<statement>" e dc s
   = dc  newenv  s
     where newenv=(identifier i) union(location,prok):
       (cont c, store s)answer:
       if i="<ident>" then cc "<statement>" newenv c s
       else e i c s

 ee "( <exp> )"  e  k  s  = ee "<exp>"  e  k  s

 ee "<ident>"    e  k  s  = k( s(e<"<ident>")),  s)

 ee "<integer>"  e  k  s  = k( value("<integer>"),  s)

 ee "<exp1>+<exp2>" e k s  = ee "<exp1>" e rhs s
   where rhs= (value v1, store s)answer:
     ee "<exp2>" e op s
     where op = (value v2, store s)answer:
       k(v1+v2, s)

     other operators similarly

 new = (store s)location:
   (int l:=0; while s(l) /= unbound do l+:=1 od; l)

To execute a program   "<statement>":

 cc "<statement>"  emptyenv  finish  emptystore
   where emptyenv  = (identifier i)union(location,prok):undefined id
   and   finish    = (store s)answer:empty
   and   emptystore= (location l)value:unbound
-- Figure 2. Semantic Equations. --

I.e. The denotational semantics of the demonstration, imperative language being defined. Note that kont (expression continuations) and dcont (declaration continuations) are traditional terms in denotational semantics.

Coding Ockham's Razor, L. Allison, Springer

A Practical Introduction to Denotational Semantics, L. Allison, CUP

free op. sys.
free office suite
~ free photoshop
web browser

© L. Allison   (or as otherwise indicated),
Faculty of Information Technology (Clayton), Monash University, Australia 3800 (6/'05 was School of Computer Science and Software Engineering, Fac. Info. Tech., Monash University,
was Department of Computer Science, Fac. Comp. & Info. Tech., '89 was Department of Computer Science, Fac. Sci., '68-'71 was Department of Information Science, Fac. Sci.)
Created with "vi (Linux + Solaris)",  charset=iso-8859-1,  fetched Tuesday, 26-Oct-2021 04:24:51 AEDT.