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