Direct Semantics Expressed in Pascal
See L. Allison, A Practical Introduction to Denotational Semantics, CUP, Cambridge Computer Science Texts V23, 1986.
These semantics include declarations and also allow side-effects within expressions (which are common in imperative languages, if dangerous).
Note function EE and
function CC in particular.
program ch6(input, output);
label 99;
type {lexical objects}
alfa = packed array [1..10] of char;
symbol = (plussy, minussy, timessy, oversy,
eqsy, nesy, ltsy, lesy, gtsy, gesy,
ident, numeral,
ifsy, thensy, elsesy, whilesy, dosy,writesy,
beginsy, endsy, skipsy,
varsy, procsy,
semisy, becomessy, open, close, stopsy);
{syntactic domains}
exptype = (bexp, uexp, varr, int, ifexp);
opr = (plus, minus, times, over,
eq, ne, lt, le, gt, ge, neg);
cmdtype = (block,call,assign, semi, ifstat, whiles, writte, skip);
dectype = (declist, vardec, procdec);
exp = ^ enode;
enode = record case tag:exptype of
bexp :(o:opr; left, right:exp);
uexp :(u:opr; son:exp);
varr :(id:alfa);
int :(i:integer);
ifexp :(e1, e2, e3 :exp)
end;
cmd = ^ cnode;
dec = ^ dnode;
dnode = record case tag:dectype of
declist :(left,right:dec);
vardec :(vid:alfa);
procdec :(id:alfa; g:cmd)
end;
cnode = record case tag:cmdtype of
block :(d:dec; body:cmd);
call :(pid:alfa);
assign :(lhs, e :exp);
semi :(left,right:cmd);
ifstat :(b:exp; gtrue,gfalse:cmd);
whiles :(bw:exp; g:cmd);
writte :(op:exp);
skip :()
end;
{-----------------------------------------------------------semantic domains}
Locn = integer;
valtype = (isInt, isLocn, isProc);
Ev = ^Evrec; {Ev = Locn + Int} {expressible values}
Evrec = record case tag:valtype of
isLocn: (l:Locn);
isInt: (i:integer)
end;
Answer =^ansrec; { Answer = integer^* answers or output}
ansrec = record v:integer;
next:Answer
end;
Store = ^ storec; { Store = Ide -> Ev }
storec = record l:Locn;
v:Ev;
next:Store
end;
State = ^starec; { State = Int x Store x Answer }
starec = record free:integer;
sto:Store;
ans:Answer
end;
Dv = ^Dvrec; { Dv = Locn + Proc } {denotable values}
Env = ^ envrec; { Env = Ide -> Dv }
Dvrec = record case tag:valtype of
isLocn : (l:Locn);
isProc : (body:cmd; e:Env)
end;
envrec = record id:alfa;
binding:Dv;
next:Env
end;
EnvxState = ^exsrec;
exsrec = record e:Env; s:State end;
EvxState = ^evxsrec;
evxsrec= record v:Ev; s:State end;
var lineno:integer;
ch : char {current character};
sy : symbol {current symbol class};
word : alfa {current keyword, identifier or operator};
n : integer {value of current numeral};
startState:State;
{------------------------------------------------------------lexical-----}
procedure error(a:alfa);
begin writeln;
writeln(' error:', a,' ch=[' ,ch,'] word=[' ,word,'] n=',n:1);
goto 99
end;
function nextch:char;
var ch:char;
begin if eof then error('prem'' eof ')
else if eoln then
begin readln; writeln;
lineno:=lineno+1; write(lineno:4,':');
nextch:=' '
end
else begin read(ch); write(ch); nextch:=ch
end
end;
procedure insymbol;
var l:integer; ch2:char;
begin while ch=' ' do ch:=nextch;
if ch in ['a'..'z','A'..'Z'] then
begin l:=0; word:=' ';
while ch in ['a'..'z','A'..'Z','0'..'9'] do
begin l:=l+1;
if l <= 10 then word[l]:=ch;
ch:=nextch
end;
if word = 'begin ' then sy:=beginsy
else if word = 'end ' then sy:=endsy
else if word = 'if ' then sy:=ifsy
else if word = 'then ' then sy:=thensy
else if word = 'else ' then sy:=elsesy
else if word = 'while ' then sy:=whilesy
else if word = 'do ' then sy:=dosy
else if word = 'skip ' then sy:=skipsy
else if word = 'var ' then sy:=varsy
else if word = 'proc ' then sy:=procsy
else if word = 'write ' then sy:=writesy
else sy:= ident
end
else if ch in ['0'..'9'] then
begin n:=0;
while ch in ['0'..'9'] do
begin n:=n*10+ord(ch)-ord('0');
ch:=nextch
end;
sy:=numeral
end
else if ch in ['+', '-', '*', '/', '=', '(', ')', ';', '.'] then
begin case ch of
'+': sy:=plussy;
'-': sy:=minussy;
'*': sy:=timessy;
'/': sy:=oversy;
'=': sy:=eqsy;
'(': sy:=open;
')': sy:=close;
';': sy:=semisy;
'.': sy:=stopsy
end;
ch:=nextch
end
else if ch in ['<' , '>', ':'] then
begin ch2:=ch; ch:=nextch;
case ch2 of
'<' : if ch='=' then sy:=lesy
else if ch='>' then sy:=nesy else sy:=ltsy;
'>': if ch='=' then sy:=gesy else sy:=gtsy;
':': if ch='=' then sy:=becomessy
else error('no = in :=')
end;
if sy in [lesy,nesy,gesy,becomessy] then ch:=nextch
end else error('insymbol ')
end {insymbol};
procedure check(s:symbol; chs:alfa);
var m:alfa;
begin if sy=s then insymbol
else begin m:='chck( )';
m[6]:=chs[1]; m[7]:=chs[2]; m[8]:=chs[3];
m[9]:=chs[4]; error(m)
end end;
function nextsymis(s:symbol):boolean;
begin nextsymis:=true;
if sy=s then insymbol else nextsymis:=false
end;
function consexp(t:exptype; f:opr; ee1,ee2:exp):exp;
var e:exp;
begin new(e); consexp:=e;
with e^ do
begin tag := t; o:=f;{hope pc doesn't check}
left:=ee1; right:=ee2
end end;
function conscmd(t:cmdtype; ctrle:exp; g1,g2:cmd):cmd;
var c:cmd;
begin new(c); conscmd:=c;
with c^ do
begin tag:=t;
case t of
block,assign: error('cons cmd ');
semi: begin left:=g1; right:=g2 end;
ifstat: begin b:=ctrle; gtrue:=g1; gfalse:=g2 end;
whiles: begin bw:=ctrle;g:=g1 end;
writte: op:=ctrle;
skip:
end end end;
function consdec(t:dectype; i:alfa; gg:cmd; d1, d2:dec):dec;
var d:dec;
begin new(d); consdec:=d;
with d^ do
begin tag:=t;
case t of
declist : begin left:=d1; right:=d2 end;
vardec : vid:=i;
procdec : begin id:=i; g:=gg end
end end end;
{-----------------------------------------------------parser--------------}
function parser:cmd;
function pexp:exp;
var e, eone, etwo :exp; o:opr;
function pexp1:exp;
var e:exp; o:opr;
function pexp2:exp;
var e:exp; o:opr;
function pexp3:exp;
var e:exp;
begin if sy=open then
begin insymbol;
e:=pexp;
check(close, ') ')
end
else if sy=minussy then
begin insymbol;
e:=consexp(uexp, neg, pexp3, nil)
end
else if sy=ident then
begin new(e);
with e^ do
begin tag:=varr; id:=word
end;
insymbol
end
else if sy=numeral then
begin new(e);
with e^ do
begin tag:=int; i:=n
end;
insymbol
end
else error('pexp3 ');
pexp3:=e
end {pexp3};
begin {pexp2}
e:=pexp3;
while sy in [timessy,oversy] do
begin if sy=timessy then o:=times
else o:=over;
insymbol;
e:=consexp(bexp, o, e, pexp3)
end;
pexp2:=e
end {pexp2};
begin {pexp1}
e:=pexp2;
while sy in [plussy,minussy] do
begin if sy=plussy then o:=plus
else o:=minus;
insymbol;
e:=consexp(bexp, o, e, pexp2)
end;
pexp1:=e
end {pexp1};
begin {pexp}
if nextsymis(ifsy) then
begin eone:=pexp; check(thensy,'Cexp ');
etwo:=pexp; check(elsesy,'Cexp ');
new(e);
with e^ do
begin tag:=ifexp; e1:=eone; e2:=etwo; e3:=pexp
end end
else
begin e:=pexp1;
if sy in [eqsy .. gesy] then
begin case sy of
eqsy: o:=eq; nesy: o:=ne;
ltsy: o:=lt; lesy: o:=le;
gtsy: o:=gt; gesy: o:=ge
end;
insymbol;
e:=consexp(bexp, o, e, pexp1)
end;
end;
pexp:=e
end {pexp};
function pcmd:cmd;forward;
function pdec:dec;
var d:dec; x:alfa;
begin if sy in [procsy, varsy] then
begin
if nextsymis(varsy) then
begin d:=consdec(vardec, word, nil, nil, nil);
insymbol
end
else {procsy}
begin insymbol; x:=word; insymbol;
check(eqsy,'pr=c ');
d:=consdec(procdec, x, pcmd, nil, nil)
end;
check(semisy,'dec; ');
d:=consdec(declist, ' ', nil, d, pdec)
end
else d:=nil;
pdec:=d
end;
function pcmd {:cmd forward-ed};
var c, cpart :cmd; lh :exp;
dpart :dec;
x:alfa;
function ifcmd:cmd;
var e:exp; g1:cmd;
begin e:=pexp;
check(thensy, 'then '); g1:=pcmd;
check(elsesy, 'else ');
ifcmd:=conscmd(ifstat,e,g1,pcmd)
end {ifcmd};
function whilecmd:cmd;
var e:exp;
begin e:=pexp; check(dosy, 'do ');
whilecmd:=conscmd(whiles, e, pcmd,nil)
end;
begin if sy=ident then
begin x:=word;
insymbol;
if nextsymis(becomessy) then
begin new(lh);
with lh^ do
begin tag:=varr; id:=x
end;
new(c);
with c^ do {lh:=rhs}
begin tag:=assign; lhs:=lh; e:=pexp
end end
else {call}
begin new(c);
with c^ do
begin tag:=call; pid:=x
end end
end
else if sy = open then { (exp):=... or syntax not LL(n) }
begin lh:=pexp; check(becomessy,'no:= ');
new(c);
with c^ do {lhs:=rhs}
begin tag:=assign; lhs:=lh; e:=pexp
end end
else if nextsymis(ifsy) then
c:=ifcmd
else if nextsymis(whilesy) then
c:=whilecmd
else if nextsymis(writesy) then
c:=conscmd(writte, pexp, nil, nil)
else if nextsymis(beginsy) then
begin dpart:=pdec;
cpart:=pcmd;
while nextsymis(semisy) do
cpart:=conscmd(semi, nil, cpart, pcmd);
check(endsy, 'end ');
new(c);
with c^ do
begin tag:=block; d:=dpart; body:=cpart end
end
else if nextsymis(skipsy) then
c:=conscmd(skip, nil,nil,nil)
else error('parse cmd ');
pcmd := c
end {pcmd};
begin {parser}
parser:=pcmd;
if sy <> stopsy then error('no . ')
end {parser};
{-------------------------------------------------------------semantics--}
procedure display(s:State);
procedure disp(m:Store);
begin if m=nil then writeln(' finish')
else begin write(' [', m^.l:3, ']=', m^.v^.i:3); disp(m^.next)
end end;
procedure prout(a:Answer);
begin if a <> nil then begin write(a^.v:4); prout(a^.next)
end end;
begin write('ans=['); prout(s^.ans); writeln(']');
disp(s^.sto)
end;
function consSta(f:integer; s:Store; a:Answer):State;
var p:State;
begin new(p); consSta:=p;
with p^ do begin free:=f; sto:=s; ans:=a end
end;
function pairEnvSta(e:Env; s:State):EnvxState;
var p:EnvxState;
begin new(p); pairEnvSta:=p;
p^.e:=e; p^.s:=s
end;
function pairEvSta(v:Ev; s:State):EvxState;
var p:EvxState;
begin new(p); pairEvSta:=p;
p^.v:=v; p^.s:=s
end;
function LocnDv(l:Locn):Dv;
var p:Dv;
begin new(p); LocnDv:=p;
p^.tag:=isLocn; p^.l:=l
end;
function ProcDv(e:Env;g:cmd):Dv;
var p:Dv;
begin new(p); ProcDv:=p;
p^.tag:=isProc; p^.e:=e; p^.body:=g
end;
function IntEv(i:integer):Ev;
var p:Ev;
begin new(p); IntEv:=p;
p^.tag:=isInt; p^.i:=i
end;
function LocnEv(l:Locn):Ev;
var p:Ev;
begin new(p); LocnEv:=p;
p^.tag:=isLocn; p^.l:=l
end;
function undefEv:Ev;
{not a function in the semantics; a fn here to get side-effect of stop}
begin undefEv:=nil {else pc complains}; error('run:undfEv') end;
function undefDv:Dv;
{see above}
begin undefDv:=nil; error('run:undfDv') end;
procedure wrong;
{run time errors}
begin error('run: wrong') end;
function updateSto(s:Store; l:Locn; val:Ev):Store;
var p:Store;
begin new(p); p^.next:=s; updateSto:=p;
p^.l:=l; p^.v:=val
end;
function applySto(s:Store; l:Locn):Ev;
begin if s=nil then applySto := undefEv
else if s^.l = l then applySto:=s^.v
else applySto:=applySto(s^.next, l)
end;
function reserve(s:State):State;
var p:State;
begin new(p);
p^:=s^; p^.free:=p^.free+1; reserve:=p
end;
function updateEnv(e:Env; id:alfa; b:Dv):Env;
var newe:Env;
begin new(newe); newe^.next:=e; updateEnv:=newe;
newe^.id:=id; newe^.binding:=b
end;
function YYEnv(e:Env):Env;
{ for a recursive function }
begin e^.binding^.e := e; YYEnv:=e end;
function applyEnv(e:Env; id:alfa):Dv;
begin if e=nil then applyEnv:=undefDv {undeclared identifier}
else if e^.id=id then applyEnv:=e^.binding
else applyEnv:=applyEnv(e^.next, id)
end;
function appendAns(a:Answer; v:Ev):Answer;
var p:Answer;
begin new(p); appendAns:=p;
if v^.tag <> isInt then wrong;
if a=nil then begin p^.v:=v^.i; p^.next:=nil end
else begin p^.v:=a^.v; p^.next:=appendAns(a^.next, v) end
end;
function LL(e:exp; exs:EnvxState):EvxState; forward;
function RR(e:exp; exs:EnvxState):EvxState; forward;
function EE(e:exp; exs:EnvxState):EvxState; {: exp x Env x State -> EvxState }
var denv:Dv; vxst:EvxState;
v1xs1, v2xs2 :EvxState;
function OO(o:opr; v1, v2 :Ev):Ev; { :opr x Ev x Ev -> Ev }
var i1, i2 :integer;
begin
if (v1^.tag <> isInt) or (v2^.tag <> isInt) then
wrong
else
begin i1:=v1^.i; i2:=v2^.i;
case o of
plus: OO:= IntEv(i1+i2);
minus:OO:= IntEv(i1-i2);
times:OO:= IntEv(i1*i2);
over: OO:= IntEv(i1 div i2);
eq: OO:= IntEv(ord(i1=i2));
ne: OO:= IntEv(ord(i1 <> i2));
lt: OO:= IntEv(ord(i1 < i2));
le: OO:= IntEv(ord(i1 <= i2));
gt: OO:= IntEv(ord(i1 > i2));
ge: OO:= IntEv(ord(i1 >= i2))
end {case}
end
end {OO};
begin {EE}
case e^.tag of
varr: begin denv:=applyEnv(exs^.e, e^.id);
case denv^.tag of
isLocn: EE:=pairEvSta(LocnEv(denv^.l), exs^.s);
isProc: wrong
end end;
int: EE:= pairEvSta(IntEv(e^.i), exs^.s);
uexp: begin vxst:= RR(e^.son, exs);
EE:= pairEvSta( IntEv( -vxst^.v^.i), vxst^.s)
end;
bexp: begin v1xs1:= RR(e^.left, exs);
v2xs2:= RR(e^.right, pairEnvSta(exs^.e,v1xs1^.s));
EE:=pairEvSta( OO(e^.o,v1xs1^.v,v2xs2^.v), v2xs2^.s)
end;
ifexp: begin vxst:=RR(e^.e1, exs);
if vxst^.v^.i = 1 then
EE:=EE(e^.e2, pairEnvSta(exs^.e,vxst^.s))
else EE:=EE(e^.e3, pairEnvSta(exs^.e,vxst^.s))
end
end {case}
end {EE};
function LL; { :exp -> Env -> State -> Ev x State }
var vxs :EvxState;
begin vxs := EE(e, exs);
case vxs^.v^.tag of
isInt: wrong;
isLocn: LL:=vxs
end end;
function RR; { :exp -> Env -> State -> Ev x State }
var vxs : EvxState; contents:Ev;
begin vxs := EE(e, exs);
case vxs^.v^.tag of
isInt: RR:=vxs;
isLocn: begin contents:=applySto(vxs^.s^.sto,vxs^.v^.l);
RR:=pairEvSta(contents, vxs^.s)
end
end end;
function DD(d:dec; exs:EnvxState):EnvxState;
begin if d=nil then DD:=exs {block may have no declns}
else case d^.tag of
declist:{d1; d2}DD:=DD(d^.right, DD(d^.left, exs));
vardec :{var x}
DD:=pairEnvSta(updateEnv(exs^.e,d^.vid,LocnDv(exs^.s^.free)),
reserve(exs^.s));
procdec:{proc id=g fixed-pt for recursive procs}
DD:=pairEnvSta(YYEnv(updateEnv(exs^.e, d^.id, ProcDv(nil{YY},d^.g))),
exs^.s)
end end;
{ State = Int x Store x Answer }
function CC(g:cmd; exs:EnvxState):State; {: cmd x Env x State -> State}
var denv:Dv; v1xs1, v2xs2 :EvxState;
begin {Main interpreter routine}
case g^.tag of
block: CC:=CC(g^.body, DD(g^.d, exs));
call: begin denv:=applyEnv(exs^.e, g^.pid);
case denv^.tag of
isLocn:wrong;
isProc:CC:=CC(denv^.body,pairEnvSta(denv^.e,exs^.s))
end end;
assign: begin v1xs1:=LL(g^.lhs, exs);
case v1xs1^.v^.tag of
isInt: wrong;
isLocn:begin v2xs2:=RR(g^.e,pairEnvSta(exs^.e,v1xs1^.s));
CC:=consSta(v2xs2^.s^.free,
updateSto(v2xs2^.s^.sto,v1xs1^.v^.l,v2xs2^.v),
v2xs2^.s^.ans)
end end end;
semi: CC:=CC(g^.right, pairEnvSta(exs^.e, CC(g^.left, exs)) );
ifstat: begin v1xs1:=RR(g^.b, exs);
if v1xs1^.v^.i = 1 then
CC:=CC(g^.gtrue, pairEnvSta(exs^.e, v1xs1^.s))
else
CC:=CC(g^.gfalse,pairEnvSta(exs^.e, v1xs1^.s))
end;
whiles: begin v1xs1:=RR(g^.bw, exs);
if v1xs1^.v^.i = 1 then
CC:=CC(g, pairEnvSta(exs^.e,
CC(g^.g, pairEnvSta(exs^.e, v1xs1^.s)) ))
else
CC:=exs^.s
end;
writte: begin v1xs1 := RR(g^.op, exs);
CC:= consSta(v1xs1^.s^.free, v1xs1^.s^.sto,
appendAns( v1xs1^.s^.ans, v1xs1^.v) )
end;
skip: CC:=exs^.s
end {case}
end {CC};
{-----------------------------------------------------------------main---}
begin
writeln(' A Pure Language, L.Allison U.W.A.');
lineno:=1; write(lineno:4, ':');
word:='-starting-'; n:=0; ch:=nextch; insymbol;
new(startState);
with startState^ do
begin free:=0; sto:=nil; ans:=nil end;
display( CC(parser, pairEnvSta({Env=}nil,startState) ) );
99: {fin}
end.