ClassicJavascript
This document describes a CEKS semantics for the core of Javascript. It's missing some details, but it contains the essential features of the language, based off of the ECMA specification. The semantics is still a work in progress. It's relatively consistent, but has some unfinished meta-function definitions and reduction rules, and still needs documentation.
Yes, I guess this means I prefer my calculi Classic.
Syntactic Categories
Expressed values:
v ::= k
| o
| rf
rf ::= ref(l,a)
| ref^v(str)
| unknownref(str)
Primitives:
k ::= undefined | null | true | false | str | n
Objects (prototype, function closure, property table reference):
o ::= object(o_parent?, c?, l_table)
Stored values:
Sv ::= v
| r
Environments/Object Tables:
r ::= [] | r[x=(l,a)]
Store:
S ::= [] | S[Sv/l]
Function closures (reside within functional objects):
c ::= (\^x(x1, ..., xn) { var y1, ..., ym; s }, r)
Attribute sets:
a in Pow({ReadOnly, DontDelete})
Program:
p ::= var x1, ..., xn; s
Expressions:
e ::= k
| function x(x1, ..., xn) { var y1, ..., ym; s }
| p(e1, ..., en)
| e(e1, ..., en)
| new e(e1, ..., en)
| e = e
| e1[e2]
| x
| pe
Primitive functions:
p ::= +
| < | ==
| ! | && | ||
| pn
Native functions:
pn ::= #ToString | #ToNumber
| #ToPrimitiveS | #ToPrimitiveN
| #DefaultString | #DefaultNumber
| #TryConversion // requires #IfPrimitive context
Statements:
s ::= if e s1 else s2
| return e;
| s1 ; s2
| e;
Expression contexts:
K ::= K o F
| KL o ([], e1.r, ..., en.r) CTX CARLIST
| Ks o Fs
Statement contexts:
Ks ::= []
| Ks o [] ; s.r CTX BEGIN
| K o call []
List contexts:
KL ::= K o FL
| KL o (v . [*]) CTX CDRLIST
Expression context frames : expval -> expval
F ::= [](e1.r, ..., en.r) FRM RATOR
| new [] (e1.r, ..., en.r) FRM CTOR
| [] = e.r FRM SETREF
| v = [] FRM SETVAL
| [][ep.r] FRM OBJ
| v[[]] FRM PROP
| #IfPrimitive [] e.r
Statement context frames : expval -> void
Fs ::= return []; FRM RETURN
| if [] s1.r else s2.r FRM CONDITION
| []; FRM DISCARD
List context frames : listof(expval) -> expval
FL ::= p.r([*]) FRM PRIM
| v([*]) FRM RANDS
| new v ([*]) FRM NEWRANDS
Meta-Functions
// Types:
// val = primitive U object
// expval = val U ref
// TODO: who all needs DontDelete?
// [8.6.2.1] Get : store * object * string -> expval
Get(S, object(_, _, l_table), str_p) = S(lp)
where r = S(l_table)
(lp,_) = r(str_p)
Get(S, object(o_parent, _, l_table), str_p) = Get(S, o_parent, str_p)
where r = S(l_table)
str_p not in dom(r)
Get(S, object(none, _, l_table), str_p) = undefined
where r = S(l_table)
str_p not in dom(r)
// TODO: abstract out Get, Put to deal with special classes for primitive types
// OK, fine, make them a slot in objects like in the spec
// [8.6.2.2] Put : store * object * string * expval -> store
Put(S, object(_, _, l_table), str_p, v) = S
where r = S(l_table)
(_,a) = r(str_p)
ReadOnly in a
Put(S, object(_, _, l_table), str_p, v) = S[v/lp]
where r = S(l_table)
(lp,a) = r(str_p)
ReadOnly not in a
Put(S, object(_, _, l_table), str_p, v) = S[v/lp, r[str_p=(lp,{})]/l_table]
where r = S(l_table)
str_p not in dom(r)
lp not in dom(S)
// [8.7.1] GetValue : expval * store -` val
GetValue(v, S) = case v of
object(_, _, _) => v
k => v
ref^vo(str_p) => Get(S, vo, str_p)
ref(l) => S(l)
unknownref(str_p) =>
where object(_, _, l_table) = o_global
r = S(l_table)
(l,_) = r(str_p)
// [8.7.2] PutValue : store * ref * expval -> store
PutValue(S, rf, v) = case rf of
ref(l) => S[v/l]
ref^vo(str_p) => Put(S, vo, str_p, v)
unknownref(str_p) => Put(S, o_global, str_p, v)
// [11.2.3, 13.2.1] PushActivation : object * object * listof(val) * store
// -> statement * environment * store
PushActivation(o_this, o_f, (v_r1, ..., v_rn), S) = <s, r', S'>
where o_f = object(_, (\^x(x1, ..., xm) { var y1, ..., ym' ; s}, r), _)
k = max(n, m)
l_this, l_args, l_argstable, l_length, l_callee not in dom(S)
l_x, l_1, ..., l_k not in dom(S)
l_y1, ..., l_ym' not in dom(S)
v_ai = if (i <= n) then v_ri else undefined [1 <= i <= k]
o_args = object(o_Object, none, l_argstable)
r_args = ["length"=(l_length,{}),
"callee"=(l_callee,{}),
"0"=(l_1,{}),
...
"n-1"=(l_n,{})]
a = { DontDelete }
r' = r[this=(l_this,{}), arguments=(l_args,a)]
[x=(l_x,a), x1=(l_x1,a), ..., xm=(l_xm,a)]
[y1=(l_y1,a), ..., ym'=(l_ym',a)]
S' = S[n/l_length, o_f/l_callee, o_args/l_args, r_args/l_argstable]
[o_f/l_x, v_a1/l_1, ..., v_ak/l_k]
[undefined/l_y1, ..., undefined/l_ym']
// [13.2.2] MakeObject : object * store -> object * store
MakeObject(oc, S) = <object(o_proto, none, l_table), S'>
where l_table not in dom(S)
v_proto = Get(S, oc, "prototype")
o_proto = case v_proto of
object(_, _, _) => v_proto
_ => o_Object
S' = S[[]/l_table]
// [13.2] MakeClosure : expression * environment * store -` object * store
MakeClosure(function x(x1, ..., xn) { var y1, ..., ym; s }, r, S) =
<object(of, S''[o_proto/l_proto, r_table/l_table])>
where l_table, l_proto not in dom(S)
<o_proto, S'> = MakeObject(o_Object, S)
of = object(o_Function,
(\^x(x1, ..., xn) { var y1, ..., ym; s }, r),
l_table)
S'' = Put(S', o_proto, "constructor", of)
r_table = ["prototype"=(l_proto,{})]
// [8.6.2, 13.2, 13.2.2, 15] Class : object -> string
Class(object(o_parent, _, _)) = case o_parent of
o_Function => "Function"
o_String => "String"
o_Boolean => "Boolean"
o_Number => "Number"
_ => "Object"
// [9.3] PrimitiveToNumber : primitive -> number
PrimitiveToNumber(undefined) = 0 // actually, should be NaN
PrimitiveToNumber(null) = 0
PrimitiveToNumber(true) = 1
PrimitiveToNumber(false) = 0
PrimitiveToNumber(n) = n
PrimitiveToNumber(str) = ParseNumber(str)
// [9.8] PrimitiveToString : primitive -> string
PrimitiveToString(undefined) = "undefined"
PrimitiveToString(null) = "null"
PrimitiveToString(true) = "true"
PrimitiveToString(false) = "false"
PrimitiveToString(n) = UnparseNumber(n)
PrimitiveToString(str) = str
// [9.3.1] ParseNumber : string -> number
// [9.8.1] UnparseNumber : number -> string
// [9.2] ToBoolean : val -> boolean
ToBoolean(v) = case v of
undefined => false
null => false
true => true
false => false
0 => false
n => true
"" => false
str => true
object(l) => true
// [9.9] ToObject : val * store -` object * store
// TODO: implement us
ToObject(v, S) = case v of
true => <o, S'>
where o = ...
false => <o, S'>
where o = ...
n => <o, S'>
where o = ...
str => <o, S'>
where o = ...
o => <o, S>
// Escape : statement-context -` expression-context
Escape(Ks) = case Ks of
Ks o [] ; s.r => Escape(Ks)
K o call [] => K
Reduction Rules
// TODO: delete
// TODO: eval-program; top-level vars are DontDelete
// TODO: need to use ToObject
1. (s, r, Ks, S) : execute Ks[s.r,S]
(if e s1 else s2, r, Ks, S) -> (e, r, Ks o if [] s1.r else s2.r, S)
(return e, r, Ks, S) -> (e, r, Ks o return [], S)
(s1 ; s2, r, Ks, S) -> (s1, r, Ks o [] ; s2, S)
(e;, r, Ks, S) -> (e, r, Ks o [];, S)
2. (e, r, K, S) : evaluate K[e.r,S]
(k, r, K, S) -> (k, K, S)
(function x(x1, ..., xn) body, r, K, S) -> (v, K, S')
where <v, S'> = MakeClosure(function x(x1, ..., xn) body, r, S)
(p(e1, ..., en), r, K, S) -> ((e1, ..., en), r, K o p([*]), S)
(e(e1, ..., en), r, K, S) -> (e, r, K o [](e1.r, ..., en.r), S)
(new e(e1, ..., en), r, K, S) -> (e, r, K o new [](e1.r, ..., en.r), S)
(e1 = e2, r, K, S) -> (e1, r, K o [] = e2.r, S)
(e1[e2], r, K, S) -> (e1, r, K o [][e2.r], S)
(x, r, K, S) -> (ref(l,a), K, S)
where (l,a) = r(x)
(x, r, K, S) -> (unknownref(Name(x)), K, S)
where x not in dom(r)
3. ((e1, ..., en), r, KL, S) : evaluate KL[(e1, ..., en).r.S]
((), r, KL, S) -> ((), KL, S)
((e1, e2, ..., en), r, KL, S) -> (e1, r, KL o ([], e2.r, ..., en.r), S)
4. (Ks, S) : return to Ks, i.e., Ks[S]
([], S) -> S
(KS o [] ; s.r, S) -> (s, r, KS, S)
(K o call [], S) -> (undefined, K, S)
5. (v, K, S) : return v to K, i.e., K[v.S]
(v, K o [](e1.r, ..., en.r), S) -> ((e1, ..., en), r, K o v([*]), S)
(v, K o new [](e1.r, ..., en.r), S) -> ((e1, ..., en), r, K o new v([*]), S)
(v, K o [] = e.r, S) -> (e, r, K o v = [], S)
(v, K o v' = [], S) -> (v'', K, S')
where v'' = GetValue(v, S)
S' = PutValue(S, v', v'')
(v, K o [][e.r], S) -> (e, r, K o v.r[[]], S)
(strp, K o v'.r[[]], S) -> (ref^v''(strp), K, S)
where v'' = GetValue(v', S)
(v, K o v'.r[[]], S) -> (#ToString(v''), r, K o v'.r[[]], S)
where v'' = GetValue(v, S)
(v, KL o ([], e1.r, ..., en.r), S) -> ((e1, ..., en), r, KL o (v . [*]), S)
(v, Ks o return [];, S) -> (v', Escape(Ks), S)
where v' = GetValue(v, S)
(v, Ks o if [] s1.r else s2.r, S) -> (s1, r, Ks, S)
where GetValue(v, S) = true
(v, Ks o if [] s1.r else s2.r, S) -> (s2, r, Ks, S)
where GetValue(v, S) = false
(v, Ks o [];, S) -> (Ks, S)
(k, K o #IfPrimitive [] e.r, S) -> (k, K, S)
(v, K o #IfPrimitive [] e.r, S) -> (e, r, K, S)
where v != k
6. ((v1, ..., vn), KL, S) : return (v1, ..., vn) to KL, i.e., KL[(v1, ..., vn).S]
((v1, ..., vn), K o ref^vo(strp)([*]), S) -> (s, r', K o call [], S')
where vm = GetValue(ref^vo(strp), S)
vi' = GetValue(vi, S)
<s, r', S'> = PushActivation(vo, vm, (v1', ..., vn'), S)
((v1, ..., vn), K o vf([*]), S) -> (s, r', K o call [], S')
where vf' = GetValue(vf, S)
vi' = GetValue(vi, S)
<s, r', S'> = PushActivation(o_global, vf', (v1', ..., vn'), S)
((v1, ..., vn), K o new vc([*]), S) -> (s, r', K', S'')
where vc' = GetValue(vc, S)
<vo, S'> = MakeObject(vc', S)
vi' = GetValue(vi, S)
<s, r', S''> = PushActivation(vo, vc', (v1', ..., vn'), S)
K' = K o call [] o ([] ; return vo;) o []; o call []
((v1, ..., vn), KL o (v . [*]), S) -> ((v, v1, ..., vn), KL, S)
// TODO: implement us!
((v1, v2), K o +.r([*]), S) ->
((v1, v2), K o <.r([*]), S) ->
((v1, v2), K o ==.r([*]), S) ->
((v), K o !.r([*]), S) ->
((v1, v2), K o &&.r([*]), S) ->
((v1, v2), K o ||.r([*]), S) ->
((o), K o #DefaultNumber.r([*]), S) -> (e, r, K, S)
where e = #TryConversion(o, "valueOf", "toString")
((o), K o #DefaultString.r([*]), S) -> (e, r, K, S)
where e = #TryConversion(o, "toString", "valueOf")
((v), K o #ToPrimitiveN.r([*]), S) -> (k, K, S)
where k = GetValue(v, S)
((v), K o #ToPrimitiveN.r([*]), S) -> (#DefaultNumber(o), r, K, S)
where o = GetValue(v, S)
((v), K o #ToPrimitiveS.r([*]), S) -> (k, K, S)
where k = GetValue(v, S)
((v), K o #ToPrimitiveS.r([*]), S) -> (#DefaultString(o), r, K, S)
where o = GetValue(v, S)
((v), K o #ToString.r([*]), S) -> (str, K, S)
where k = GetValue(v, S)
str = PrimitiveToString(k)
((v), K o #ToString.r([*]), S) -> (#ToPrimitiveS(o), r, K', S)
where o = GetValue(v, S)
K' = K o #ToString.r([*]) o ([])
((v), K o #ToNumber.r([*]), S) -> (n, K, S)
where k = GetValue(v, S)
n = PrimitiveToNumber(k)
((v), K o #ToNumber.r([*]), S) -> (#ToPrimitiveN(o), r, K', S)
where o = GetValue(v, S)
K' = K o #ToNumber.r([*]) o ([])
((o, str_p, v1, ..., vn), K o #TryConversion.r, S) -> (o, K', S)
where om = Get(S, o, str_p)
e_cont = #TryConversion(o, v1, ..., vn)
K' = K o #IfPrimitive [] e_cont.r o []()
