|
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.
|
|