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 []()