Figure 2

home1 home2
 Bib
 Algorithms
 Bioinfo
 FP
 Logic
 MML
 Prog.Lang
and the
 Book

 Comp.J.1985

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

Linux
 Ubuntu
free op. sys.
OpenOffice
free office suite
The GIMP
~ free photoshop
Firefox
web browser

© L. Allison   http://www.allisons.org/ll/   (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 Saturday, 30-Mar-2024 00:25:57 AEDT.