Syntactic Categories
I in Ident (identifiers) L in Lexp (l-expressions, or references) E in Exp (expressions, commands) P in Prog (full programs)Syntax BNF
L ::= I E ::= 0 | 1 | I | !L | E1; E2 | (E1 + E2) | let I = E1 in E2 end | new I := E1 in E2 end | L := E | if E1 then E2 else E3 | while E1 do E2 P ::= program (I) ; E end .Value Domains
n in Int = { ..., -2, -1, 0, 1, 2, ... } (integers) alpha in Loc (no structure details...) sigma in States = Loc --> Int U {unused} (states, of memory) rho in Env = Ident --> Int U Loc U {undef}Semantic Functions
LL : Lexp --> Env --> States --> Loc MM : Exp --> Env --> States --> (Int * States) PP : Prog --> Int --> IntSemantic Equations
LL [ I ] rho sigma = rho(I) PP [ program (I); E end. ] n = let fun rho(J) = undef fun sigma(alpha') = unused alpha be some Loc such that sigma(alpha) = unused (v,sigmaF) = MM [[ E ]] rho[I |-> alpha] sigma[alpha |-> n] in sigmaF(alpha) end MM [ 0 ] rho sigma = (0,sigma) MM [ 1 ] rho sigma = (1,sigma) MM [ I ] rho sigma = (rho(I),sigma) MM [ !L ] rho sigma = let alpha = LL [ L ] rho sigma in (sigma(alpha),sigma) end MM [ E1 + E2 ] rho sigma = let (n,sigma') = MM [E1] rho sigma (m,sigma") = MM [E2] rho sigma' in (plus(n,m),sigma") end MM [ if E1 then E2 else E3 ] rho sigma = let (n,sigma') = MM [E1] rho sigma in ite(n=0, MM [E2] rho sigma', MM [E3] rho sigma' ) end MM [ E1; E2 ] rho sigma = let (n,sigma') = MM [E1] rho sigma in MM [E2] rho sigma' end (* note that n, the value of E1, is discarded *) MM [[ while E1 do E2 ]] rho sigma = let fun p(sigma') = let (b,sigma") = MM [E1] rho sigma' (m,sigma''') = MM [E2] rho sigma" in ite(b=0, p(sigma'") else (b,sigma") ) end in p(sigma) end MM [ let I=E1 in E2 end ] rho sigma = let (n,sigma') = MM [E1] rho sigma rho' = rho[I |-> n] in MM [E2] rho' sigma' end MM [ L := E ] rho sigma = let alpha = LL [ L ] rho sigma (n,sigma') = MM [E] rho sigma in (n,sigma'[alpha |-> n]) end MM [ new I := E1 in E2 end ] rho sigma = let (n,sigma') = MM [E1] rho sigma alpha be some Loc such that sigma'(alpha) = unused in MM [E2] rho[I |-> alpha] sigma'[alpha |-> n] end