Figure 2

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

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.