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 | function I1 (I2) = E1 in E2 end | call I (E) 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) f in Func = States --> Int --> (Int * States) rho in Env = Ident --> Int U Loc U Func U {undef}Semantic Functions
LL : Lexp --> Env --> States --> Loc MM : Exp --> Env --> States --> (Int * States) PP : Prog --> Int --> IntSemantic Equations
(* include all from previous example *) (* plus these new ones *) MM [ function I1 (I2) = E1 in E2 end ] rho sigma = let f sigma' n = MM [E1] rho[I2 |-> n] sigma' in MM [E2] rho[I1 |-> f] sigma end (* environment for function eval is bound at definition time *) MM [ call I (E) ] rho sigma = let (n,sigma') = MM [E] rho sigma f = rho(I) in f sigma' n end