^Semantics^ ^examples^

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.




© L. Allison, School of Computer Science and Software Engineering, Monash University, Australia 3800.
Created with "vi (Linux & IRIX)",   charset=iso-8859-1