This is the result of an effort to define a formal small step operational semantics strictly conforming to the ECMAScript (ECMA262-3) specification. For a discussion, see the technical report "An operational semantics for JavaScript". Comments are welcome ().
Last revision: November 6, 2014.
[Show All]
t !< {t1,...,tn} means t is different from each ti. t < {t1,...,tn} means t=ti for some i. !A means logical negation of A. A U B means union. A!=B means A different from B. A=B means equality; e.g. {m:5}.m = 5. |t1,...,tn| = n. |"c1...cn"| = n. In a grammar, [t] means that t is optional and t|s means either t or s. In a grammar, we escape with apices, as in escaping [ by "[" and we omit '' when the meaning is clear from the context. t~ = t1,...,tn non empty. t* = t1 ... tn or empty. t+ = t1 ... tn non empty. (op), where op < {+,-,...} denotes the ECMA 262 specification of an arithmetic function with some intuitive behaviour. "_" denotes anything that can be parsed until the next delimiter ";" or ")", as in "for(_) s". When C is a context containing a hole "-", C[t] denotes C with t substituted for "-". H' = H[l<-o] means redefining H at l with o. L ranges over lists of heap addresses. [] is the empty list, l:L a list with head l and tail L. When the meaning is clear from the context, we write "n+1" to denote the numeral obtained by adding 1 to the number denoted by the numeral "n" (instead of meaning the expression "n + 1". Reserved Words (RW) = { this, new, function, delete, void, typeof, instanceof, in, var, if, else, while, do, for, continue, break, return, with, switch, case, default, throw, try, catch, finally }
H ::= (l:o)~ % heap l ::= #x % heap addresses x ::= foo | bar | ... % identifiers (do not include reserved words) c ::= m | n | b | null % literals m ::= "foo" | "bar" | ... % strings n ::= -n | &NaN | &Infinity | 0 | 1 | ... % numbers b ::= true | false % booleans o ::= "{"[(i:ov)~]"}" % objects i ::= m | @x % indexes ov ::= va["{"a~"}"] | fun"("[x~]"){"P"}" | L % object values a ::= ReadOnly| DontEnum | DontDelete % attributes va ::= pv | l % pure values pv ::= c | &undefined % primitive values r ::= ln"*"m % references ln ::= l | null % nullable addresses v ::= va | r % values vae ::= &empty | va % value or empty xe ::= &empty | x % identifier or empty ls ::= "{"[xe~]"}" % label sets w ::= "|"va"|" % exception lw ::= l | w % address or exception vw ::= v | w % value or exception vaw ::= va | w % pure value or exception pvw ::= pv | w % primitive value or exception bw ::= b | w % boolean or exception co ::= "("ct,vae,xe")" % completions ct ::= Normal | Break | Continue % completion type | Return | Throw pn ::= n | m | x % property name
e ::= this % the "this" object x % identifier pv % primitive value "[" [(e|,)~] "]" % array literal "{"[(pn:e)~]"}" % object literal "("e")" % parenthesis expression e.x % property accessor e"["e"]" % member selector new e["("[e~]")"] % constructor invocation e"("[e~]")" % function invocation function [x] "("[x~]"){"[P]"}" % [named] function expression e &PO % postfix operator &UN e % unary operators e &BIN e % binary operators "("e"?"e":"e")" % conditional expression "("e","e")" % sequential expression % internal expressions l % hence va r % hence v w % hence vw pv &+ pv % sum, not cocatenation @AddProps(e[,(pn:e)~]) % GetValue and ToString context, adds properties to a literal object @TS(e) % context for a ToString @TN(e) % context for a ToNumber @TP(e) % context for a ToPrimitive @GV(e) % context for a GetValue @Fun(l,e[,va~]) % function call @PO(v,e,n) % context for ToNumber, postfix operators @Typeof(e) % typeof operator @"<"S(b,va,va) % ToPrimitive context, relational operators @"<"N(b,va,va) % ToNumber context, relational operators @L(b,va,va,e) % ToBoolean context, binary logical operators @ArrayLiteral(e,n,([e~])) % initialization of array literals l.@Call(vaw[,va~]) % internal call property (function call) l.@Exe(l[,e~]) % execution of native functions @FunExe(l,P) % execution of user function body l.@Construct([e,][va~]) % internal constructor property (new) @ConstructCall(l,e) % helper for Construct l.@DefaultValue([String|Number]) % internal default value (type conversions) @GetDefault(l,m,e) % helper for DefaultValue @cEval(P) % eval helper @FunParse(m,e[,va~]) % parse body in fucntion constructor @PutValue(v,va) @GetValue(r) @ExeFPA(l,vaw,va) l.@Put(l,m,va) @PutLen(l,n) % operators &PO < {"++","--"} &UN < {delete,void,typeof,"++","--","+","-","~","!"} &BIN < {"*","/","%", "+","-", "<<",">>",">>>", "<",">","<=",">=","instanceof","in", "==","!=","===","!==", "&","^","|", "&&","||", "=",&O"="} &O < {"*","/","%","+","-","<<",">>",">>>","&","^","|"} &A < {"*","/","%","-",&+,"<<",">>",">>>"} &E < {"==","==="} &B < {"&","^","|"} &L < {"&&","||"} &OP < {"<",">","<=",">=","+",&A,&E,&B,instanceof,in}
s ::= "{"s*"}" % block var [(x["="e])~] % assignment ; % skip e % expression not starting with "{","function" if "("e")" s [else s] % conditional while "("e")" s % while do s while "("e")"; % do-while for "("e in e")" s % for-in for "("var x["="e] in e")" s % for-var-in continue [x]; % continue break [x]; % break return [e]; % return with "("e")" s % with id:s % label throw e; % throw try "{"s*"}" [catch "("x"){"s1*"}"] [finally "{"s2*"}"] % try % internal statements co % completion @while(e,s,ls,vae,e,s) % used for while @Block(co[,s+]) % used for blocks @VarList([e,][x[=e]~]) % used for variable declarations @with (l,ln,ln,s) % used for with @eforin(e,ls,s,vae,l,e,m) @pforin(e,ls,s,vae,l,m) @sforin(e,ls,s,vae,l,s,m) ls>s % label-set
P ::= % programs fd [P] % function declaration s [P] % statement fd ::= function x "("[x~]"){"[P]"}" % function declaration
T ::= % Types % public types - primitive Undefined Null Boolean String Number % public types - object Object % internal types Reference
TYPE: alloc: (H,o) -> H,l TYPE: -(-): (H,l) -> o TYPE: del: (H,l,i) -> H TYPE: -(-.-=-): (H,l,i,ov) -> H TYPE: -.-=-: (o,i) -> va TYPE: -:-=-: (o,i) -> {[a~]} TYPE: - !< -: (i,o) TYPE: - < -: (i,o) %%% Heap functions l !< H H1 = H,l:o ----------------- [H-alloc] alloc(H,h) = H1,l l:o < H -------- [H-ret] H(l) = o o = {(i1:ov1)~[,i:l1],(i2:ov2)~} o1 = {(i1:ov1)~,(i2:ov2)~} H(l) = o H1 = H[l<-o1] i !< i1~,i2~ --------------------------------- [H-del] del(H,l,i) = H1 o = {(i1:ov1)~[,i:ov0],(i2:ov2)~} o1 = {(i1:ov1)~,i:ov,(i2:ov2)~} H(l) = o H1 = H[l<-o1] i !< i1~,i2~ ---------------------------------- [H-set] H(l.i=ov) = H1 {(i1:ov1)~,i:va[{a~}],(i2:ov2)~}.i = va [H-get] {(i1:ov1)~,i:va[{[a~]}],(i2:ov2)~}:i = {[a~]} [H-attr] {(i1:ov1)~,i:fun([x~]){P},(i2:ov2)~}-i = fun([x~]){P} [H-fun] i !< i~ -------------- [H-notin] i !< {(i:ov)~} i < i~ ------------- [H-isin] i < {(i:ov)~}
TYPE: Prototype: (H,ln,m)->ln TYPE: Scope: (H,ln,m)->ln %%% Property Lookup: prototype and scope chain Prototype(H,null,m)=null [Prototype-null] m < H(l) ------------------ [Prototype-ref] Prototype(H,l,m)=l m!< H(l) H(l).@Prototype=ln ---------------------------------- [Prototype-lookup] Prototype(H,l,m)=Prototype(H,ln,m) H,l.@HasProperty(m) ------------------- [Scope-ref] Scope(H,l,m)=l !(H,l.@HasProperty(m)) H(l).@Scope=ln -------------------------- [Scope-lookup] Scope(H,l,m)=Scope(H,ln,m) Scope(H,null,m)=null [Scope-null]
new_object(m,l) = { @Class: m, @Prototype: l } new_proto(m,l1,l2{a~}) = { @Class: m, @Prototype: l1, "constructor": l2{a~} } new_function(fun([x~]){P},L,l1) = { "prototype": l1{DontDelete}, @Prototype: #FunctionProt, @Class: "Function", @Call: true, @Construct: true, @FScope: L, @Body: fun([x~]){P}, "length": |x~|{DontDelete,ReadOnly,DontEnum} } new_arguments(n,([va1,...,van]),l) = { ["1": va1{DontEnum}, ... "n": van{DontEnum},] @argumentsFlag: true, @Prototype: #ObjectProt, "callee": l{DontEnum}, "length": n{DontEnum} } new_activation(l1,l2,l3) = { @Scope: l3, @Prototype: null, @IsActivation: true, @this: l2, "arguments": l1{DontDelete} }
TYPE: -,-.@Get(-): (H,l,m) -> va TYPE: -,-.@CanPut(-): (H,l,m) -> b TYPE: -,-.@HasProperty(-): (H,l,m) -> b TYPE: -,-.@HasInstance(-): (H,l,va) -> [H],bw TYPE: -,-.@Delete(-): (H,l,m) -> H,b Prototype(H,l,m)=l1 H(l1).m=va ---------------- [I-Get] H,l.@Get(m) = va Prototype(H,l,m)=null ------------------------ [I-Get-null] H,l.@Get(m) = &undefined Prototype(H,l,m)=l1 ReadOnly < H(l1):m ---------------------- [I-CanPut-not] H,l.@CanPut(m) = false Prototype(H,l,m)=l1 ReadOnly !< H(l1):m --------------------- [I-CanPut-yes] H,l.@CanPut(m) = true Prototype(H,l,m)=null --------------------- [I-CanPut-null] H,l.@CanPut(m) = true H,l.@HasProperty(m) = (Prototype(H,l,m)!=null) [I-HasProperty] H,l.@Get("prototype")=l2 H(l1).@Prototype = l2 --------------------------- [I-HasInstance] H,l.@HasInstance(l1) = true H,l.@Get("prototype")=l2 H(l1).@Prototype = l3 l3 != l2 ------------------------------------------- [I-HasInstance-rec] H,l.@HasInstance(l1) = H,l.@HasInstance(l3) H,l.@Get("prototype")=pv o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) --------------------------------------- [I-HasInstance-Exc] H,l.@HasInstance(l1) = H2,|l2| H,l.@HasInstance(pv) = false [I-HasInstance-not] m !< H(l) ----------------------- [I-Delete-empty] H,l.@Delete(m) = H,true DontDelete < H(l):m ------------------------ [I-Delete-not] H,l.@Delete(m) = H,false DontDelete !< H(l):m del(H,l,m)=H1 ------------------------ [I-Delete-yes] H,l.@Delete(m) = H1,true
TYPE: Join: (vae,vae) -> vae TYPE: GetNextProperty: (H,l,l,n) = m TYPE: FP: (H,k,{[a~]},([x~]),n,n) -> H TYPE: FPN: (([va~]),n,([va~])) -> ([va~]) TYPE: VD: (H,l,{[a~]}[,P]) -> H TYPE: FD: (H,l,{[a~]}[,P]) -> H TYPE: Function: (H,fun([x~]){P},l) -> (H,l) TYPE: CopyScope: (H,ln) -> L TYPE: PasteScope: (H,L) -> H TYPE: SetScope: (l,l,H) -> H,ln,ln TYPE: FindScope: (ln,l,H) -> ln bmk % Propagating values in loops Join(vae,&empty) = vae [H-Join-empty] Join(vae,va) = va [H-Join] % Enumerating properties in for-in [&ImplementationDependent] ------------------------------ [H-GetNextProperty] GetNextProperty(H,l1,l2,i) = m GetNextProperty(H,l1,l2,m) = &stop [H-GetNextProperty-stop] % Formal parameters FP(H,l,{[a~]},(),n1,n2) = H [H-FP] n1 < n2 l1 = H(l)."arguments" va = H(l1)."n1" H(l."x"=va{[a~]}) = H1 -------------------------------------------------------------- [H-FP-actual] FP(H,l,{[a~]},(x[,x~]),n1,n2) = FP(H1,l,{[a~]},([x~]),n1+1,n2) n1 >= n2 H(l."x"=&undefined{[a~]}) = H1 -------------------------------------------------------------- [H-FP-formal] FP(H,l,{[a~]},(x[,x~]),n1,n2) = FP(H1,l,{[a~]},([x~]),n1+1,n2) % Formal parameters for native functions FPN(([va~]),0,([va1~])) = ([va1~]) [H-FPN] FPN((va[,va~]),n+1,([va1~])) = FPN(([va~]),n,([va1~,]va)) [H-FPN-actual] FPN((),n+1,([va1~])) = FPN((),n,([va1~,]&undefined)) [H-FPN-formal] % Variable instantiation VD(H,l,{[a~]}) = H [H-VD] "x" !< H(l) H(l."x"=&undefined{[a~]}) = H1 -------------------------------------------------------------------------------- [H-VD-init] VD(H,l,{[a~]},var x[=v][,(xt[=vt])~] [P]) = VD(H1,l,{[a~]},var [(xt[=vt])~] [P]) "x" < H(l) ------------------------------------------------------------------------------- [H-VD-init-ignore] VD(H,l,{[a~]},var x[=v][,(xt[=vt])~] [P]) = VD(H,l,{[a~]},var [(xt[=vt])~] [P]) VD(H,l,{[a~]},var [P]) = VD(H,l,{[a~]}[,P]) [H-VD-var] VD(H,l,{[a~]},{s*} [P]) = VD(H,l,{[a~]},s* [P]) [H-VD-block] VD(H,l,{[a~]},if (e) s1 else s2 [P]) = VD(H,l,{[a~]},s1 s2 [P]) [H-VD-if] VD(H,l,{[a~]},while (e) s [P]) = VD(H,l,{[a~]},s [P]) [H-VD-while] VD(H,l,{[a~]},do s while (e); [P]) = VD(H,l,{[a~]},s [P]) [H-VD-dowhile] VD(H,l,{[a~]},for (_) s [P]) = VD(H,l,{[a~]},s [P]) [H-VD-for] VD(H,l,{[a~]},with (e) s [P]) = VD(H,l,{[a~]},s [P]) [H-VD-with] VD(H,l,{[a~]},try {s*} [catch (x){s1*}] [finally {s2*}] [P]) = VD(H,l,{[a~]},s* [s1*] [s2*] [P]) [H-VD-try] s < {";",e,"continue [x];","break [x];","return [e];","throw e;"} ---------------------------------------------------------------------- [H-VD-ignore] VD(H,l,{[a~]},s [P]) = VD(H,l,{[a~]}[,P]) % Function declarations FD(H,l,{[a~]}) = H [H-FD] H,Function(fun([x~]){; [P]},l) = H1,l1 H1(l."x"=l1{[a~]}) = H2 --------------------------------------------------------------- [H-FD-fd] FD(H,l,{[a~]},function x([x~]) {[P]} P1) = FD(H2,l,{[a~]}[,P1]) s !< {while,for, ... function} ----------------------------------------- [H-FD-ignore] FD(H,l,{[a~]},s [P]) = FD(H,l,{[a~]}[,P]) % Function object creation p = new_object("Object",#ObjectProt) H1,l1 = alloc(H,p) L = CopyScope(H1,l) o = new_function(fun([x~]){P},L,l1) H2,l2 = Alloc(H1,o) H3 = H2(l1."constructor"=l2{DontEnum}) -------------------------------------- [H-Function] H,Function(fun([x~]){P},l) = H3,l2 % Auxiliary function used by the H-Function rule [null] = CopyScope(H,null) [CopyScope-Null] H(l).@Scope = ln L = Copyscope(H,ln) -------------------------- [CopyScope] l:L = CopyScope(H,l) % Update the scope chain H = PasteScope(H,[null]) [PasteScope-Null] H1 = H(l1.@Scope) = l2 H2 = PasteScope(H1,l2:L) -------------------------- [PasteScope] H2 = PasteScope(H,l1:l2:L) % Auxiliary functions used by the @with internal statement l <> l1 FindScope(l,l1,H) = l2 H(l1).@Scope = l3 H(l2.@Scope=l3{}) = H2 H2(l1.@Scope=l{}) = H1 --------------------------- SetScope(l,l1,H) = H1,l3,l2 l <> l1 FindScope(l,l1,H) = null H(l1).@Scope = l2 H(l1.@Scope=l{}) = H1 --------------------------- SetScope(l,l1,H)=H1,l2,null l <> l1 FindScope(l,l1,H) = null @Scope !< H(l1) H(l1.@Scope=l{}) = H1 ------------------------------- SetScope(l,l1,H) = H1,null,null l = l1 ------------------------------ SetScope(l,l1,H) = H,null,null FindScope(null,l,H) = null H(l).@Scope = l2 l2 <> l1 -------------------------------------- FindScope(l,l1,H) = FindScope(l2,l1,H) H(l).@Scope = l1 --------------------- FindScope(l,l1,H) = l ResetScope(l,null,null,H) = H H(l1.@Scope=l2{}) = H1 -------------------------- ResetScope(l1,l2,null,H) = H1 H(l1.@Scope=l2{}) = H1 H1(l3.@Scope=l1{}) = H2 ------------------------ ResetScope(l1,l2,l3,H) = H2
TYPE: Type: v -> T TYPE: TypeConv: T -> m TYPE: IsPrim: v -> b TYPE: IsError: v -> b TYPE: GetType: H,v -> m TYPE: IsNativeFun: l -> b TYPE: IsNativeObj: l -> b TYPE: IsNativeConstr: l -> b TYPE: IsVariableLen: l -> b TYPE: IsActivation: H,l -> b TYPE: IsHost: H,l -> b Type(-) &undefined = Undefined null = Null b = Boolean m = String n = Number % non primitive cases ln*m = Reference l = Object TypeConv(-) = - Undefined = "undefined" Null = "object" Boolean = "boolean" String = "string" Number = "number" IsPrim(v) = Type(v) !< {Reference,Object} [T-Isprim] IsError(H,v) = (v=) [T-Iserror] TypeConv(pv) = m ----------------- [T-GetType-prim] GetType(H,pv) = m @Call < H(l) @Host !< H(l) !IsNativeFun(l) ------------------------- [T-GetType-fun] GetType(H,l) = "function" @Call !< H(l) @Host !< H(l) !IsNativeFun(l) ----------------------- [T-GetType-obj] GetType(H,l) = "object" @Host < H(l) !IsNativeFun(l) -------------------------------------- [T-GetType-host] GetType(H,l) = &ImplementationDependent IsNativeFun(l) ------------------------- [T-GetType-native] GetType(H,l) = "function" % Nativity tests IsNativeFun(l) = (l < NativeFunctions) [T-NativeFun] IsNativeObj(l) = (l < NativeObjects) [T-Native-Obj] IsNativeConstr(l) = (l < NativeConstr) [T-NativeConstr] IsVariableLen(l) = (l < VariableLen) [T-VariableLen] IsActivation(H,l) = (@isActivation < H(l)) IsHost(H,l) = (@Host < H(l))
TYPE: ToPrimitive: va[,T]->e TYPE: ToBoolean: va->b TYPE: ToNumber: va->e TYPE: ToString: va->e TYPE: ToObject: (H,va)->H,lw TYPE: StringNumber: m -> n TYPE: NumberString: n -> m Type(l)=Object ----------------------------------------- [TC-ToPrimitive-obj] ToPrimitive(l[,T]) = l.@DefaultValue([T]) Type(pv)!=Object ----------------------- [TC-ToPrimitive-obj] ToPrimitive(pv[,T]) = pv Type(v)=Object ------------------- [TC-ToBoolean-obj] ToBoolean(v) = true Type(v)=Number v<{0,-0,&NaN} -------------------- [TC-ToBoolean-num] ToBoolean(v) = false Type(v)=Number v!<{0,-0,&NaN} ------------------- [TC-ToBoolean-num] ToBoolean(v) = true Type(v)=String v="" -------------------- [TC-ToBoolean-str] ToBoolean(v) = false Type(v)=String v!="" -------------------- [TC-ToBoolean-str] ToBoolean(v) = true Type(v)=Boolean ---------------- [TC-ToBoolean-bool] ToBoolean(v) = v Type(v)=Null -------------------- [TC-ToBoolean-null] ToBoolean(v) = false Type(v)=Undefined -------------------- [TC-ToBoolean-undef] ToBoolean(v) = false Type(v)=Object ---------------------------------------- [TC-ToNumber-obj] ToNumber(v) = @TN(ToPrimitive(v,Number)) Type(v)=Number --------------- [TC-ToNumber-num] ToNumber(v) = v Type(v)=String n=StringNumber(v) ----------------- [TC-ToNumber-str] ToNumber(v) = n Type(v)=Boolean v=true ---------------------- [TC-ToNumber-bool] ToNumber(v) = 1 Type(v)=Boolean v=false ----------------------- [TC-ToNumber-bool] ToNumber(v) = 0 Type(v)=Null --------------- [TC-ToNumber-null] ToNumber(v) = 0 Type(v)=Undefined ------------------ [TC-ToNumber-undef] ToNumber(v) = &NaN Type(v)=Object ---------------------------------------- [TC-ToString-obj] ToString(v) = @TS(ToPrimitive(v,String)) Type(v)=Number m = NumberString(v) ------------------- [TC-ToString-num] ToString(v) = m Type(v)=String --------------- [TC-ToString-str] ToString(v) = v Type(v)=Boolean ----------------- [TC-ToString-bool] ToString(v) = "v" Type(v)=Null -------------------- [TC-ToString-null] ToString(v) = "null" Type(v)=Undefined ------------------------- [TC-ToString-undef] ToString(v) = "undefined" Type(v)=Object ------------------- [TC-ToObject-obj] ToObject(H,v) = H,v Type(v)=Number o = new_Number(v) H1,l1= alloc(H,o) --------------------- [TC-ToObject-num] ToObject(H,v) = H1,l1 Type(v)=String o = new_String(v) H1,l1= alloc(H,o) --------------------- [TC-ToObject-str] ToObject(H,v) = H1,l1 Type(v)=Boolean o = new_Boolean(v) H1,l1= alloc(H,o) --------------------- [TC-ToObject-bool] ToObject(H,v) = H1,l1 Type(v)=Null o = new_native_error("",#TypeErrorProt) H1,l1= alloc(H,o) --------------------------------------- [TC-ToObject-Exc-null] ToObject(H,v) = H1,|l1| Type(v)=Undefined o = new_native_error("",#TypeErrorProt) H1,l1= alloc(H,o) --------------------------------------- [TC-ToObject-Exc-undef] ToObject(H,v) = H1,|l1|
TYPE: @Put: (l,m,va) -> va TYPE: @GetValue: v->vaw TYPE: @PutValue: v,va->vaw TYPE: @DefaultValue: [T] -> pvw TYPE: @GetDefault: (l,m,e) -> pvw TYPE: @Construct: [va~] -> l TYPE: @ConstructCall: (l,v) -> l TYPE: @Call: l,[va~] -> va H(l1).@Class != "Array" !(H,l1.@CanPut(m)) --------------------------- [I-Put-not] H,l,l1.@Put(m,va) -> H,l,va H(l1).@Class != "Array" H,l1.@CanPut(m) m !< H(l1) H(l1.m=va{})=H1 ---------------------------- [I-Put-create] H,l,l1.@Put(m,va) -> H1,l,va H(l1).@Class != "Array" H,l1.@CanPut(m) H(l1):m={[a~]} H(l1.m=va{[a~]}) = H1 ---------------------------- [I-Put-replace] H,l,l1.@Put(m,va) -> H1,l,va Type(l1*m)=Reference H,l1.@Get(m)=va --------------------------- [R-GetValue-ref] H,l,@GetValue(l1*m) = H,l,va Type(null*m)=Reference o = new_native_error("",#ReferenceErrorProt) H2,l2= alloc(H,o) -------------------------------------------- [R-GetValue-Exc] H,l,@GetValue(null*m) = H2,l,|l2| Type(va)=!Reference ------------------------- [R-GetValue-val] H,l,@GetValue(va) = H,l,va Type(v)!=Reference o = new_native_error("",#ReferenceErrorProt) H1,l1= alloc(H,o) -------------------------------------------- [R-PutValue-Exc] H,l,@PutValue(v,va) -> H1,l,|l1| Type(null*m)=Reference -------------------------------------------------- [R-PutValue-null] H,l,@PutValue(null*m,va) -> H,l,#Global.@Put(m,va) Type(l1*m)=Reference ------------------------------------------- [R-PutValue-val] H,l,@PutValue(l1*m,va) -> H,l,l1.@Put(m,va) % Default value % PrimitiveValue, Exception % @GetDefault % Fixing a bug in the spec (8.6.2.6) that erroneously requests Type(l2)=Object instead of @Call < H(l2) H,l1.@Get("toString")=l2 @Call < H(l2) -------------------------------------------------------------------------- [I-DefaultValue-String-obj] H,l,l1.@DefaultValue(String) -> H,l,@GetDefault(l1,"valueOf",l2.@Call(l1)) H,l1.@Get("valueOf")=l2 @Call < H(l2) ----------------------------------------------------------------------------- [I-DefaultValue-Number-obj] H,l,l1.@DefaultValue([Number]) -> H,l,@GetDefault(l1,"toString",l2.@Call(l1)) H,l1.@Get("toString")=va Type(va)!=Object ---------------------------------------------------------------- [I-DefaultValue-String] H,l,l1.@DefaultValue(String) -> H,l,@GetDefault(l1,"valueOf",va) H,l1.@Get("valueOf")=va Type(va)!=Object ------------------------------------------------------------------- [I-DefaultValue-Number] H,l,l1.@DefaultValue([Number]) -> H,l,@GetDefault(l1,"toString",va) H,l,@GetDefault(l1,m,pv) -> H,l,pv [I-GetDefault-pv] m!="fail" !IsPrim(v) H,l1.@Get(m)=l2 @Call < H(l2) ------------------------------------------------------------------ [I-GetDefault-next] H,l,@GetDefault(l1,m,v) -> H,l,@GetDefault(l1,"fail",l2.@Call(l1)) m="fail" !IsPrim(v) o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) --------------------------------------- [I-GetDefault-Exc-fail] H,l,@GetDefault(l1,m,v) -> H2,l,|l2| m!="fail" !IsPrim(v) H,l1.@Get(m)=va !@Call < H(va) o = new_native_error("",#TypeErrorProt) H3,l3= alloc(H,o) --------------------------------------- [I-GetDefault-Exc] H,l,@GetDefault(l1,m,v) -> H3,l,|l3| % @Call % Value,Exception,Reference % @Exe,@FunExe IsNativeFun(l1) !IsVariableLen(l1) H(l1)."length" = n FPN(([va~]),n,()) = ([va1~]) |va~| = n1 H1 = H(l1.@Actuals=n1) ------------------------------------------------ [I-Call-Native] H,l,l1.@Call(l2[,va~]) -> H1,l,l1.@Exe(l2,[va1~]) IsNativeFun(l1) IsVariableLen(l1) |va~| = n1 H1= H(l1.@Actuals=n1) ----------------------------------------------- [I-Call-Native-Var] H,l,l1.@Call(l2[,va~]) -> H1,l,l1.@Exe(l2,[va~]) !IsNativeFun(l1) H(l1).@Body = fun([x~]){P} |[va~]| = n L = CopyScope(H,l) new_arguments(n,([va~]),l1) = args alloc(H,args) = H1,l3 H1(l1).@FScope = l4:L1 H2 = PasteScope(H1,l4:L1) new_activation(l3,l2,l4) = act alloc(H2,act) = H3,l5 FP(H3,l5,{DontDelete},([x~]),0,n) = H4 VD(H4,l5,{DontDelete},P) = H5 FD(H5,l5,{DontDelete},P) = H6 -------------------------------------------- [I-Call] H,l,l1.@Call(l2[,va~]) -> H6,l5,@FunExe(L,P) H1 = PasteScope(H,l1:L) --------------------------------------------- [I-Fun-Exc] H,l,@FunExe(l1:L,(Throw,va,xe)) -> H1,l1,|va| H1 = PasteScope(H,l1:L) -------------------------------------------- [I-Fun-Ret] H,l,@FunExe(l1:L,(Return,va,xe)) -> H1,l1,va H1 = PasteScope(H,l1:L) ----------------------------------------------------- [I-Fun] H,l,@FunExe(l1:L,(Normal,vae,xe)) -> H1,l1,&undefined % @Construct % Object,Exception % @ConstructCall l2 = H(l1)."prototype" Type(l2)=Object o = new_object("Object",l2) H3,l3 = Alloc(H,o) !IsNativeConstr(l1) ---------------------------------------------------------------------- [I-Construct] H,l,l1.@Construct([va~]) -> H3,l,@ConstructCall(l3,l1.@Call(l3,[va~])) pv = H(l1)."prototype" Type(pv)!=Object o = new_object("Object",#ObjectProt) H2,l2 = Alloc(H,o) ---------------------------------------------------------------------- [I-Construct-Global] H,l,l1.@Construct([va~]) -> H2,l,@ConstructCall(l2,l1.@Call(l2,[va~])) Type(l2) = Object ----------------------------------- [I-CCall-obj] H,l,@ConstructCall(l1,l2) -> H,l,l2 Type(v) != Object ---------------------------------- [I-CCall-v] H,l,@ConstructCall(l1,v) -> H,l,l1
% this % Object Scope(H,l,@this)=l1 H,l1.@Get(@this)=va ------------------- [E-This] H,l,this -> H,l,va % identifier % Reference Scope(H,l,"x")=ln ------------------- [E-Ide-val] H,l,x -> H,l,ln*"x" % literals % Null, Boolean, Number, String % regular expression literals % Reference, Exception % arrays % [Object or Reference], Exception % @ArrayLiteral H,l,"["[(e|,)~]"]" -> H,l,@ArrayLiteral(new Array(),0,([(e|,)~])) [E-Array] H,l,@ArrayLiteral(l1,n,()) -> H,l,(l1.@Put("length",n),l1) [E-AL] H,l,@ArrayLiteral(l1,n,(,[(e|,)~])) -> H,l,@ArrayLiteral(l1,n(+)1,([(e|,)~])) [E-AL-skip] H,l,@ArrayLiteral(l1,n,(va[,(e|,)~])) -> H,l,@ArrayLiteral((l1.@Put("n",va),l1),n(+)1,([(e|,)~])) [E-AL-init] % Literal object % Object, Exception % @AddProps H,l,{[(pn:e)~]} -> H,l,@AddProps(new Object()[,(pn:e)~]) [E-Obj] H,l,@AddProps(l1,x:e[, (pn:e)~]) -> H,l,@AddProps(l1,"x":e[, (pn:e)~]) [E-@AddProps-ide] H,l,@AddProps(l1,m:va[, (pn:e)~]) -> H,l,@AddProps((l1.@Put(m,va),l1)[,(pn:e)~]) [E-@AddProps-ind] H,l,@AddProps(l1) -> H,l,l1 [E-@AddProps-empty] % parenthesis % Value, Exception H,l,(v) -> H,l,v [E-Par] % property accessors % selection % Reference, Exception H,l,e.x -> H,l,e["x"] [E-Sel] % member access % Reference, Exception H,l,l1[m] -> H,l,l1*m [E-Acc] % new operator % Object, Exception % @Construct Type(va)!=Object o = new_native_error("",#TypeErrorProt) H1,l1= alloc(H,o) --------------------------------------- [E-New-Exc-ojb] H,l,new va[([va~])]-> H1,l,|l1| Type(l1)=Object @Construct !< H(l1) o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) --------------------------------------- [E-New-Exc-constr] H,l,new l1[([va~])]-> H2,l,|l2| Type(l1)=Object @Construct < H(l1) ---------------------------------------------- [E-New-constr] H,l,new l1[([va~])]-> H,l,l1.@Construct([va~]) % function calls % Object, Exception % @Fun, @Call Type(ln*m) = Reference !isActivation(H,ln) ------------------------------------------ [E-Call-Ref] H,l,ln*m([va~]) -> H,l,@Fun(ln,ln*m[,va~]) Type(ln*m) = Reference isActivation(H,ln) ----------------------------------------------- [E-Call-Ref-Act] H,l,ln*m([va~]) -> H,l,@Fun(#Global,ln*m[,va~]) Type(va) != Reference ------------------------------------------- [E-Call] H,l,va([va~]) -> H,l,@Fun(#Global,va[,va~]) GetType(H,va) != "function" o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) --------------------------------------- [E-@Fun-Exc] H,l,@Fun(l1,va[,va~]) -> H2,l,|l2| GetType(H,l2) = "function" ----------------------------------------------- [E-@Fun-Call] H,l,@Fun(l1,l2[,va~]) -> H,l,l2.@Call(l1[,va~]) % function expression % Object H,Function(fun([x~]){; [P]},l) = H1,l1 ------------------------------------------------- [E-Fun] H,l,function ([x~]) {[P]} -> H1,l,l1 o = new_object("Object",#ObjectProt) H1,l1 = Alloc(H,o) H1(l1.@Scope=l{}) = H2 H2,Function(fun([x~]){; [P]},l1) = H3,l3 H3(l1.name="x"{DontDelete,ReadOnly}) = H4 ---------------------------------------- [E-Fun-Named] H,l,function x([x~]) {[P]} -> H4,l,l3 % postfix increment/decrement % Number % @PO H,l,v++ -> H,l,@PO(v,v,1) [E-postInc] H,l,v-- -> H,l,@PO(v,v,(-)1) [E-postDec] H,l,@PO(v,n1,n2) -> (v=n1+n2,n1) [E-PO] % delete % Boolean Type(va)!= Reference ------------------------- [E-Delete-true] H,l,delete va -> H,l,true Type(l1*m)= Reference H,l1.@Delete(m) = H1,b ------------------------- [E-Delete-false] H,l,delete l1*m -> H1,l,b % void % Undefined H,l,void va -> H,l,&undefined [E-void] % typeof % String, Undefined % @Typeof H,l,typeof null*m -> H,l,"undefined" [E-Typeof-null] H,l,typeof l1*m -> H,l,@Typeof(l1*m) [E-Typeof-reference] Type(va)!=Reference -------------------------------- [E-Typeof] H,l,typeof va -> H,l,@Typeof(va) GetType(H,va) = m ------------------------ [E-@Typeof] H,l,@Typeof(va) -> H,l,m % prefix increment/decrement % Number, Exception H,l,++v -> H,l,v = v+1 [E-preInc] H,l,--v -> H,l,v = v-1 [E-preDec] % unary + % Number H,l,"+"n -> H,l,n [E-plus] % unary - % Number n != &NaN -------------------- [E-minus] H,l,"-"n -> H,l,(-)n H,l,"-"&NaN -> H,l,&NaN [E-minus-NaN] % bitwise not % Number H,l,~n -> H,l,(~)n [E-BW-not] % logical not % Boolean H,l,"!"b -> H,l,(!)b [E-L-not] % aritmetic and shifting operators: &A < {"*","/","%","-",&+,"<<",">>",">>>"} % Number H,l,n1 &A n2 -> H,l,n1(&A)n2 [E-Arit] % sum % Number Type(pv1) != String Type(pv2) != String ------------------------------- [E-sum] H,l,pv1 + pv2 -> H,l,pv1 &+ pv2 % concat % String H,l,m + pv -> H,l,m + @TS(pv) [E-concat-r] H,l,pv + m -> H,l,@TS(pv) + m [E-concat-l] H,l,m1 + m2 -> H,l,m1m2 [E-concat] % relational operators % Boolean % @str, @"<"N H,l,va1"<"va2 -> H,l,@"<"S(false,va1::Number,va2::Number) [E-Rel-lt] H,l,va1">"va2 -> H,l,@"<"S(false,va2::Number,va1::Number) [E-Rel-gt] H,l,va1"<="va2 -> H,l,@"<"S(true,va1::Number,va2::Number) [E-Rel-le] H,l,va1">="va2 -> H,l,@"<"S(true,va2::Number,va1::Number) [E-Rel-ge] Type(pv1)=String Type(pv2)=String StringCompare(pv1,pv2)=b1 ---------------------------------- [E-Rel-Str] H,l,@"<"S(b,pv1,pv2) -> H,l,b(^)b1 Type(pv1)!=String -------------------------------------------- [E-Rel-L] H,l,@"<"S(b,pv1,pv2) -> H,l,@"<"N(b,pv1,pv2) Type(pv2)!=String -------------------------------------------- [E-Rel-R] H,l,@"<"S(b,pv1,pv2) -> H,l,@"<"N(b,pv1,pv2) NumberCompare(n1,n2)=b1 -------------------------------- [E-Rel-Num] H,l,@"<"N(b,n1,n2) -> H,l,b(^)b1 NumberCompare(n1,n2)=&undefined ------------------------------- [E-Rel-Num-Undef] H,l,@"<"N(b,n1,n2) -> H,l,false % instanceof % Boolean, Exception % @HasInstance Type(pv) != Object o = new_native_error("",#TypeErrorProt) H1,l1= alloc(H,o) --------------------------------------- [E-Instof-Exc-obj] H,l,va instanceof pv -> H1,l,|l1| Type(l1) = Object @HasInstance !< H(l1) o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) --------------------------------------- [E-Instof-Exc-inst] H,l,va1 instanceof l1 -> H2,l,|l2| Type(l1) = Object @HasInstance < H(l1) H,l1.@HasInstance(va) = b ------------------------------------------------ [E-Instof-HasInst] H,l,va instanceof l1 -> H,l,b Type(l1) = Object @HasInstance < H(l1) H,l1.@HasInstance(va) = H1,w ------------------------------------------------ [E-Instof-prot] H,l,va instanceof l1 -> H1,l,w % in % Boolean, Exception Type(pv) != Object o = new_native_error("",#TypeErrorProt) H1,l1= alloc(H,o) --------------------------------------- [E-In-Exc] H,l,va in pv -> H1,l,|l1| Type(l1) = Object H,l1.@HasProperty(m)=b ---------------------- [E-In] H,l,m in l1 -> H,l,b % equality operators: &E < {"==","!=","===","!=="} % Boolean,Exception % @TP, @TN H,l,e1 != e2 -> !(e1 == e2) [E-!=] Type(va1) = Type(va2) ----------------------------- [E-Eq] H,l,va1==va2 -> H,l,va1(=)va2 H,l,null==&undefined -> H,l,true [E-Eq-nu] H,l,&undefined==null -> H,l,true [E-Eq-un] Type(va1) = Number Type(va2) = String --------------------------------- [E-Eq-ns] H,l,va1==va2 -> H,l,va1==@TN(va2) Type(va1) = String Type(va2) = Number --------------------------------- [E-Eq-sn] H,l,va1==va2 -> H,l,@TN(va1)==va2 Type(va1) = Boolean Type(va2) != Boolean --------------------------------- [E-Eq-bnb] H,l,va1==va2 -> H,l,@TN(va1)==va2 Type(va1) != Boolean Type(va2) = Boolean --------------------------------- [E-Eq-nbb] H,l,va1==va2 -> H,l,va1==@TN(va2) Type(va1) < {String,Number} Type(va2) = Object --------------------------------- [E-Eq-sno] H,l,va1==va2 -> H,l,va1==@TP(va2) Type(va1) = Object Type(va2) < {String,Number} --------------------------------- [E-Eq-osn] H,l,va1==va2 -> H,l,@TP(va1)==va2 Type(va1) = Null != Type(va2) != Undefined ------------------------------------------ [E-Eq-nnu] H,l,va1==va2 -> H,l,false Type(va1) = Number != Type(va2) !< {String,Object} -------------------------------------------------- [E-Eq-nnso] H,l,va1==va2 -> H,l,false Type(va1) = String != Type(va2) != Object ------------------------------------------ [E-Eq-sno] H,l,va1==va2 -> H,l,false Type(va1) = Undefined != Type(va2) != Null ------------------------------------------ [E-Eq-unn] H,l,va1==va2 -> H,l,false Type(va1) = Object != Type(va2) !< {String,Number} -------------------------------------------------- [E-Eq-onsn] H,l,va1==va2 -> H,l,false % strict equality % Boolean,Exception H,l,e1 !== e2 -> H,l,!(e1 === e2) [E-!==] Type(va1) = Type(va2) ----------------------------- [E-SEq] H,l,va1===va2 -> H,l,va1==va2 Type(va1) != Type(va2) -------------------------- [E-SEq-false] H,l,va1===va2 -> H,l,false % binary bitwise operators: &B < {"&","^","|"} % Number H,l,n1 &B n2 -> H,l,n1(&B)n2 [E-Bitwise] % binary logical operators: &L < {"&&","||"} % PrimitiveValue,Object,Exception % @L, @GV H,l,va && e -> H,l,@L(true,va,va,e) [E-And ] H,l,va || e -> H,l,@L(false,va,va,e) [E-Or] b1(^)b2 -------------------------------- [E-@L-exit] H,l,@L(b1,b2,va,e) -> H,l,va !(b1(^)b2) ------------------------------------ [E-@L] H,l,@L(b1,b2,va,e) -> H,l,@GV(e) % conditional % PrimitiveValue,Object,Exception % @GV H,l,(true?e1:e2) -> H,l,@GV(e1) [E-Cond-true] H,l,(false?e1:e2) -> H,l,@GV(e2) [E-Cond-false] % assignment operators "=", &O < {"*","/","%","+","-","<<",">>",">>>","&","^","|"} % PrimitiveValue,Object,Exception % @PutValue H,l,v=va -> H,l,@PutValue(v,va) [E-Asgn] H,l,v &O"=" e -> H,l,v=(v &O e) [E-Asgn-Comp] % comma (e should be an Assignment expression) % PrimitiveValue,Object H,l,(va1,va2) -> H,l,va2 [E-comma]
H,l,P -> H1,l1,P1 --------------------------- [Ep-Ctx] H,l,eCp[P] -> H1,l1,eCp[P1] eCp ::= @FunExe(l,-) @cEval(-) H,l,e -> H1,l1,e1 ------------------------- [E-Ctx] H,l,eC[e] -> H1,l1,eC[e1] H,l,eC[w] -> H,l,w [E-Exc] eC ::= - (eC) eCgv @ConstructCall(l,eC) @GetDefault(l,m,eC) eC([e~]) delete eC @AddProps(-,[,(pn:e)~]) typeof eC - = e - &O"=" e - ++ - "--" ++ - "--" - H,l,eCgv[ln*m] -> H,l,eCgv[@GetValue(ln*m)] [E-GV] eCgv ::= @AddProps(l,m:-[, (pn:e)~]) -[e] va[-] new -[([e~])] new va([va~,]-[,e~]) v([va~,]-[,e~]) @Fun(ln,-[,va~]) void - @Typeof(-) - &OP e va &OP - - &L e (-,e) (va,-) @GV(-) v=- @ArrayLiteral(-,n,([e~])) @ArrayLiteral(l,n,(-[,e~])) l.@Exe(l1,[va~,]-[,e~]) l.@Construct([va~,]-[,e~]) eCtn eCto eCts eCtb eCtp &OP < {"<",">","<=",">=","+",&A,&E,&B,instanceof,in} Type(v) != String ToString(v) = e -------------------------- [E-TS] H,l,eCts[v] -> H,l,eCts[e] eCts ::= @AddProps(l,-:e[, (pn:e)~]) l[-] - in l @TS(-) @FunParse(m,-[,va~]) #String.@Construct(-) #String.@Exe(l,-) #Error.@Construct(-) #NativeError.@Construct(-) Type(va) != Object ToObject(H,va) = H1,lw ----------------------------- [E-TO] H,l,eCto[va] -> H1,l,eCto[lw] eCto ::= -[va] l.@Call(-[,va~]) @ExeFPA(l1,-,va2) Type(va) != Number ToNumber(va) = e --------------------------- [E-TN] H,l,eCtn[va] -> H,l,eCtn[e] eCtn ::= @PO(v,-,n) + - "-" - ~ - - &A va n &A - - &+ pv n &+ - @"<"N(b,-,va) @"<"N(b,n,-) - &B va n &B - @TN(-) #Number.@Exe(l,-) #Number.@Construct(-) #SfromCharCode.@Exe(l1,[n~,]-[,va~]) Type(va) != Boolean ToBoolean(va) = b --------------------------- [E-TB] H,l,eCtb[va] -> H,l,eCtb[b] eCtb ::= ! - @L(b1,-,va,e) (-?e1:e2) #Boolean.@Exe(l,-) #Boolean.@Construct(-) ToPrimitive(l1[,T]) = e -------------------------------- [E-TP] H,l,eCtp[l1[::T]] -> H,l,eCtp[e] eCtp ::= - + va pv + - @"<"S(b,-,va::T) @"<"S(b,pv,-) @TP(-) % Leaving helper contexts H,l,@GV(va) -> H,l,va [E-@GV] H,l,@TN(n) -> H,l,n [E-@TN] H,l,@TS(m) -> H,l,m [E-@TS] H,l,@TP(pv) -> H,l,pv [E-@TP]
% Blocks and Statement Lists H,l,{s*} -> H,l,@Block((Normal,&empty,&empty)[,s+]) [S-Block-Start] H,l,@Block((ct,vae,xe)) -> H,l,(ct,vae,xe) [S-Block-End] ct !< {Normal} ---------------------------------------------- [S-Block-Exc] H,l,@Block(co,(ct,vae,xe) s*) -> H,l,(ct,vae,xe) Join(vae1,vae2)=vae ------------------------------------------------------------------------------- [S-Block] H,l,@Block((ct,vae1,xe),(Normal,vae2,xe1) s*) -> H,l,@Block((Normal,vae,xe1)[,s+]) %Variable Statements H,l,var (x[=e])~ -> H,l,@VarList(x[=e]~) [S-Var] H,l,@VarList() -> H,l,(Normal,&empty,&empty) [S-Var-empty] H,l,@VarList(l1*m=va[,(x[=e])~]) -> H,l,@VarList(@PutValue(l1*m,va)[,(x[=e])~]) [S-Var-init] H,l,@VarList(v[,x[=e]~]) -> H,l,@VarList([x[=e]~]) [S-Var-ignore] % Empty statement H,l,; -> H,l,(Normal,&empty,&empty) [S-Empty] % Expression H,l,va -> H,l,(Normal,va,&empty) [S-Expr] % If then else H,l, if (true) s1 [else s2] -> H,l,s1 [S-If-true] H,l, if (false) s1 -> H,l,(Normal,&empty,&empty) [S-If-false] H,l, if (false) s1 else s2 -> H,l,s2 [S-Ife-false] % Iteration statements % While [ls U] {&empty} = ls1 ------------------------------------------------------ [S-While] H,l,[ls>]while (e) s -> H,l,@while(e,s,ls1,&empty,e,s) H,l,@while(e,s,ls,vae,false,s) -> H,l,(Normal,vae,&empty) xe < ls Join(vae1,vae2)=vae -------------------------------------------------------------------- [S-While-break] H,l,@while(e,s,ls,vae1,true,(Break,vae2,xe)) -> H,l,(Normal,vae,&empty) xe < ls Join(vae1,vae2)=vae -------------------------------------------------------------------------- [S-While-continue] H,l,@while(e,s,ls,vae1,true(Continue,vae2,xe)) -> H,l,@while(e,s,ls,vae,e,s) ct != Normal xe !< ls ----------------------------------------------------------- [S-While-abrupt] H,l,@while(e,s,ls,vae1,true,(ct,vae2,xe)) -> H,l,(ct,vae2,xe) Join(vae1,vae2)=vae ------------------------------------------------------------------------- [S-While-iter] H,l,@while(e,s,ls,vae1,true,(Normal,vae2,xe)) -> H,l,@while(e,s,ls,vae,e,s) % do While [ls U] {&empty} = ls1 -------------------------------------------------------------- [S-Do-While] H,l,[ls>] do s while (e); -> H,l,@while(e,s,ls1,&empty,true,s) % For in H,l,[ls>]for (var x[=e1] in e2) s -> H,l,{var x[=e1]; [ls>]for (x in e2) s} [S-ForVarIn] [ls U] {} = ls1 ----------------------------------------------------------------- [S-ForIn] H,l,[ls>]for (e in l1) s -> H,l,@pforin(e,ls1,s,&empty,l1,&start) GetNextProperty(H,l,l1,i) = m1 ------------------------------------------------------------- [S-pForIn-next] H,l,@pforin(e,ls,s,vae,l1,m) -> H,l,@eforin(e,ls,s,vae,l1,e,m1) GetNextProperty(H,l,l1,m) = &stop ----------------------------------------------------- [S-pForIn-stop] H,l,@pforin(e,ls,s,vae,l1,m) -> H,l,(Normal,vae,&empty) H,l,@eforin(e,ls,s,vae,l1,v,m) -> H,l,@sforin(e,ls,s,vae,l1,{@PutValue(v,m);s},m) [S-eForIn-bind] xe < ls Join(vae1,vae2)=vae --------------------------------------------------------------------- [S-sForIn-break] H,l,@sforin(e,ls,s,vae1,l1,(Break,vae2,xe),m) -> H,l,(Normal,vae,&empty) xe < ls Join(vae1,vae2)=vae ----------------------------------------------------------------------------- [S-sForIn-cont] H,l,@sforin(e,ls,s,vae1,l1,(Continue,vae2,xe),m) -> H,l,@pforin(e,ls,s,vae,l1,m) ct != Normal xe !< ls Join(vae1,vae2)=vae ----------------------------------------------------------- [S-sForIn-outer] H,l,@sforin(e,ls,s,vae1,l1,(ct,vae2,xe),m) -> H,l,(ct,vae,xe) Join(vae1,vae2)=vae ------------------------------------------------------------------------- [S-sForIn-loop] H,l,@sforin(e,ls,s,vae1,l1,(Normal,vae2,xe)) -> H,l,@pforin(e,ls,s,vae,l1,m) % Continue H,l,continue; -> H,l,(Continue,&empty,&empty) [S-Continue] H,l,continue x; -> H,l,(Continue,&empty,x) [S-Continue-id] % Break H,l,break; -> H,l,(Break,&empty,&empty) [S-Break] H,l,break x; -> H,l,(Break,&empty,x) [S-Break-id] % Return Statement H,l,return; -> H,l,(Return,&undefined,&empty) [S-Return] H,l,return va; -> H,l,(Return,va,&empty) [S-Return-expr] % With SetScope(l,l1,H) = H1,ln1,ln2 ------------------------------------------- [S-With-set] H,l,with (l1) s -> H1,l1,@with(l,ln1,ln2,s) ResetScope(l1,ln1,ln2,H) = H1 --------------------------------- [S-With-reset] H,l1,@with(l,ln1,ln2,co) -> H1,l,co % Labelled statements H,l,[ls>]id:s -> H,l,([ls U] {id})>s [S-Label] s !< {id:s1,while,...} ---------------------- [S-Label-ignore] H,l,ls>s -> H,l,s % Throw statement H,l,throw va; -> H,l,(Throw,va,&empty) [S-Throw] % Try statement H,l,try co -> H,l,co [S-Try-end] ct != Throw ------------------------------------------------------------------------------------ [S-Try-Finally] H,l,try (ct,vae,xe) catch (x) {s1} [finally {s2}]-> H,l,try (ct,vae,xe) [finally {s2}] H,l,try co finally (Normal,vae,xe) -> H,l,co [S-Finally] ct != Normal ----------------------------------------------- [S-Finally-abrupt] H,l,try co finally (ct,vae,xe) -> H,l,(ct,vae,xe) o=new_object("Object",#ObjectProt) H1,l1=alloc(H,o) H2=H1(l1."x"=va{DontDelete}) H3=H2(l1.@Scope=l{}) ---------------------------------------------------------------------------------------- [S-Try-Catch] H,l,try (Throw,va,xe) catch (x) {s1} [finally {s2}] -> H3,l1,@catch {s1} [finally {s2}] l=H(l1).@Scope H1=delete(H,l1,@Scope) ------------------------------------------------------------ [S-Catch] H,l1,@catch co [finally {s2}] -> H1,l,try co [finally {s2}]
H,l,s -> H1,l1,s1 ------------------------- [S-Ctx] H,l,sC[s] -> H1,l1,sC[s1] sC ::= - @Block(co,sC s*) @with (l,ln,ln,sC) try sC [catch (x) {s1}] [finally {s2}] @catch sC [finally {s2}] try co finally sC @while(e,s,ls,vae,true,sC) @sforin(e,ls,s,vae,lo,sC,m) H,l,e -> H1,l1,e1 --------------------------- [Se-Ctx] H,l,sCe[e] -> H1,l1,sCe[e1] H,l,sCe[|va|] -> H,l,(Throw,va,&empty) [Se-Exc] sCe ::= @VarList(-[,(x[=e])~]) sCgv @eforin(e,ls,s,vae,lo,-,m) H,l,sCgv[ln*m] -> H1,l,sCgv[@GetValue(ln*m)] [S-GV] sCgv ::= - sCto return - throw - sCtb Type(va) != Boolean ToBoolean(va) = b --------------------------- [S-TB] H,l,sCtb[va] -> H,l,sCtb[b] sCtb ::= if (-) s1 [else s2] @while(e,s,ls,vae,-,s) Type(v) != Object ToObject(H,v) = H1,lw ---------------------------- [S-TO] H,l,sCto[v] -> H1,l,sCto[lw] sCto ::= with (-) s for (e in -) s
VD(NativeEnv,#Global,{DontDelete},P) = H1 FD(H1,#Global,{DontDelete},P) = H2 ----------------------------------------- [P-Init] P -> H2,#Global,P H,l,(Normal,vae,xe) P -> H,l,P [P-Seq] IsActivation(H,l) ------------------------------------------ [P-Return] H,l,(Return,vae,xe) P -> H,l,(Return,vae,xe) !IsActivation(H,l) o = new_SyntaxError() H1,l1 = alloc(H,o) ----------------------------------------------- [P-Return-Exc] H,l,(Return,vae,xe) [P] -> H,l,(Throw,l1,&empty) H,l,(Throw,va,xe) P -> H,l,(Throw,va,xe) [P-Throw] ct < {Break,Continue} o = new_SyntaxError() H1,l1 = alloc(H,o) -------------------------------------------- [P-Exc-synt] H,l,(ct,vae,xe) [P] -> H1,l,(Throw,l1,&empty) H,l,function x ([x~]){[P]} [P1] -> H,l,(Normal,&empty,&empty) [P1] [P-Fun] H,l,s -> H1,l1,s1 ------------------------- [P-Ctx] H,l,s [P] -> H1,l1,s1 [P]
@Global = { @Prototype: &ImplementationDependent, @Class: &ImplementationDependent, @this: #Global, @Scope: null, "NaN": &Nan{DontEnum,DontDelete}, "Infinity": &Infinity{DontEnum,DontDelete}, "undefined": &undefined{DontEnum,DontDelete}, "eval": #GEval{DontEnum}, "isNaN": #isNaN{DontEnum}, "Object": #Object{DontEnum}, "Function": #Function{DontEnum}, "Array": #Array{DontEnum}, "String": #String{DontEnum}, "Boolean": #Boolean{DontEnum}, "Number": #Number{DontEnum}, "Error": #Error{DontEnum}, "NativeError": #NativeError{DontEnum}, "Math": #Math{DontEnum} } %---------------------------- Function properties of the global object % Eval @GEval,@GEvalProt = make_native_fun(#GEval,#GEvalProt,1) !ParseProg(m) = &undefined o = new_SyntaxError() H2,l2 = alloc(H,o) ---------------------------------- [N-Eval-Exc] H,l,#GEval.@Exe(l1,m) -> H2,l,|l2| GetType(H,va) != "string" -------------------------------- [N-Eval-value] H,l,#GEval.@Exe(l1,va) -> H,l,va ParseProg(m) = P VD(H,#Global,{DontDelete},P} = H1 FD(H1,#Global,{DontDelete},P) = H2 ----------------------------------------------------- [N-Eval-Global] H,#Global,#GEval.@Exe(l1,m) -> H2,#Global,@cEval(P) l != #Global ParseProg(m) = P VD(H,l,{},P} = H1 FD(H1,l,{},P) = H2 ----------------------------------------- [N-Eval-local] H,l,#GEval.@Exe(l1,m) -> H2,l,@cEval(P) Join(&undefined,vae)=v ------------------------------- [N-Eval-end] H,l,@cEval((ct,vae,xe)) -> H,l,v % isNaN @isNaN,@isNaNProt = make_native_fun(#isNaN,#isNaNProt,1) Type(va) != number ----------------------------------------------------- [N-isNaN-cast] H,l,#isNaN.@Exe(l1,va) -> H,l,#isNaN.@Exe(l1,@TN(va)) H,l,#isNaN.@Exe(l1,&NaN) -> H,l,true [N-isNaN-true] n != &NaN ---------------------------------- [N-isNaN-false] H,l,#isNaN.@Exe(l1,n) -> H,l,false
@Object = new_native_constr(#ObjectProt,1) % Object called as a function pv < {null,&undefined} --------------------------------------------------- [N-Object-fun-nullundef] H,l,#Object.@Exe(l1,pv)->H,l,#Object.@Construct(pv) va !< {null,&undefined} H1,le = ToObject(H,va) -------------------------------- [N-Object-fun] H,l,#Object.@Exe(l1,va)->H1,l,le % Object called as a constructor o = new_object("Object",#ObjectProt) H1,lo = Alloc(H,o) ------------------------------------ [N-Object-constr-nopar] H,l,#Object.@Construct() -> H1,l,lo o = new_object("Object",#ObjectProt) H1,lo = Alloc(H,o) Type(pv) < {Null,Undefined} ------------------------------------- [N-Object-constr-nullundef] H,l,#Object.@Construct(pv) -> H1,l,lo Type(l1) = Object !IsHost(H,l1) ------------------------------------ [N-Object-constr-native] H,l,#Object.@Construct(l1) -> H,l,l1 Type(l1) = Object IsHost(H,l1) ----------------------------------------------------- [N-Object-constr-host] H,l,#Object.@Construct(l1) -> &ImplementationDependent Type(pv) < {String, Boolean, Number} H1,le = ToObject(H,pv) ------------------------------------ [N-Object-constr-pv] H,l,#Object.@Construct(pv) -> H,l,le
@ObjectProt = { @Class: "Object", @Prototype: null, "constructor": #Object{DontEnum}, "toString": #OPtoString{DontEnum}, "toLocaleString": #OPtoLocaleString{DontEnum}, "valueOf": #OPvalueOf{DontEnum}, "hasOwnProperty": #OPhasOwnProperty{DontEnum}, "isPrototypeOf": #OPisPrototypeOf{DontEnum}, "propertyIsEnumerable": #OPpropertyIsEnumerable{DontEnum} } % Properties of Object.prototype @OPtoString,@OPtoStringProt = make_native_fun(#OPtoString,#OPtoStringProt,0) H(l1).@Class = m --------------------------------------------- [N-OPtoString] H,l,#OPtoString.@Exe(l1) -> H,l,"[object"m"]" @OPtoLocaleString,@OPtoLocaleStringProt = make_native_fun(#OPtoLocaleString,#OPtoLocaleStringProt,0) H,l,#OPtoLocaleString.@Exe(l1) -> H,l,l1.toString() [N-OPtoLocaleString] @OPvalueOf,@OPvalueOfProt = make_native_fun(#OPvalueOf,#OPvalueOfProt,0) !IsHost(H,l1) --------------------------------- [N-OPvalueOf] H,l,#OPvalueOf.@Exe(l1) -> H,l,l1 IsHost(H,l1) -------------------------------------------------- [N-OPvalueOf-host] H,l,#OPvalueOf.@Exe(l1) -> &ImplementationDependent @OPhasOwnProperty,@OPhasOwnPropertyProt = make_native_fun(#OPhasOwnProperty,#OPhasOwnPropertyProt,1) (m < H(l1)) = b ----------------------------------------- [N-hasOwnProperty] H,l,#OPhasOwnProperty.@Exe(l1,m) -> H,l,b Type(va) != String --------------------------------------------------------------------------- [N-hasOwnProperty-cast] H,l,#OPhasOwnProperty.@Exe(l1,va) -> H,l,#OPhasOwnProperty.@Exe(l1,@TS(va)) @OPisPrototypeOf,@OPisPrototypeOfProt = make_native_fun(#OPisPrototypeOf,#OPisPrototypeOfProt,1) Type(v) != Object -------------------------------------------- [N-isPrototypeOf-not] H,l,#OPisPrototypeOf.@Exe(l1,v) -> H,l,false Type(v) = Object H(v).@Prototype = null -------------------------------------------- [N-isPrototypeOf-null] H,l,#OPisPrototypeOf.@Exe(l1,v) -> H,l,false Type(v) = Object H(v).@Prototype = l1 ------------------------------------------- [N-isPrototypeOf-true] H,l,#OPisPrototypeOf.@Exe(l1,v) -> H,l,true Type(v) = Object H(v).@Prototype = l2 l2 !< {l1,null} ------------------------------------------------------------------ [N-isPrototypeOf-rec] H,l,#OPisPrototypeOf.@Exe(l1,v) -> H,l,#OPisPrototypeOf.@Exe(l2,v) @OPpropertyIsEnumerable,@OPpropertyIsEnumerableProt = make_native_fun(#OPpropertyIsEnumerable,#OPpropertyIsEnumerableProt,1) m !< H(l1) --------------------------------------------------- [N-propertyIsEnumerable-missing] H,l,#OPpropertyIsEnumerable.@Exe(l1,m) -> H,l,false DontEnum < H(l1):m --------------------------------------------------- [N-propertyIsEnumerable-false] H,l,#OPpropertyIsEnumerable.@Exe(l1,m) -> H,l,false DontEnum !< H(l1):m -------------------------------------------------- [N-propertyIsEnumerable-true] H,l,#OPpropertyIsEnumerable.@Exe(l1,m) -> H,l,true Type(va) != String --------------------------------------------------------------------------------------- [N-propertyIsEnumerable-cast] H,l,#OPpropertyIsEnumerable.@Exe(l1,va) -> H,l,#OPpropertyIsEnumerable.@Exe(l1,@TS(va))
@Function = new_native_constr(#FunctionProt,1) % Function called as a function H,l,#Function.@Exe(l1,[va~,]va) -> H,l,#Function.@Construct([va~,]va) [N-Function-fun] H,Function(fun(){;},#Global) = H1,l1 ------------------------------------ [N-Function-empty] H,l,#Function.@Construct() -> H,l,l1 H,l,#Function.@Construct([va~,]va) -> H,l,@FunParse("",[va~,]va) [N-Function-Parse-start] H,l,@FunParse(m1,m2[,va~],va) -> H,l,@FunParse(m1","m2[,va~],va) [N-Function-Parse-rec] ParseParams(m1) = &undefined o = new_SyntaxError() H1,l1 = alloc(H,o) ---------------------------------------- [N-Function-Exc-pars] H,l,@FunParse(m1,m2) -> H1,l,|l1| ParseParams(m1) = x~ ParseFunction(m2) = &undefined o = new_SyntaxError() H1,l1 = alloc(H,o) ---------------------------------------- [N-Function-Exc-body] H,l,@FunParse(m1,m2) -> H1,l,|l1| ParseParams(m1) = x~ ParseFunction(m2) = P H,Function(fun(x~){P},#Global) = H1,l1 ----------------------------------------- [N-Function-Parse-done] H,l,@FunParse(m1,m2) -> H1,l,l1
@FunctionProt = { @Class: "Function", @Prototype: #ObjectProt, @Call: true, @Construct: true, "prototype": #FunctionProtProt{DontDelete}, "constructor": #Function{DontEnum}, "toString: #FPtoString{DontEnum}, "apply": #FPapply{DontEnum}, "call": #FPcall{DontEnum} } @FunctionProtProt = new_proto("Object",#ObjectProt,#FunctionProt{DontEnum}) H,l,#FunctionProt.@Exe(l1) -> H,l,&undefined [N-FPExe] @FPtoString,@FPtoStringProt = make_native_fun(#FPtoString,#FPtoStringProt,0) GetType(H,l1) != "function" o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) --------------------------------------- [N-FPtoString] H,l,#FPtoString.@Exe(l1) -> H2,l,|l2| GetType(H,l1) = "function" -------------------------------------------------------- [N-FPtoString] H,l,#FPtoString.@Exe(l1) -> H1,l,&ImplementationDependent @FPcall,@FPcallProt = make_native_fun(#FPcall,#FPcallProt,1) GetType(H,l1) != "function" o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) ------------------------------------------ [N-FPcall-Exc] H,l,#FPcall.@Exe(l1,va[,va~]) -> H2,l,|l2| GetType(H,l1) = "function" va < {null,#undefined} ------------------------------------------------------------ [N-FPcall-global] H,l,#FPcall.@Exe(l1,va[,va~]) -> H,l,l1.@Call(#Global[,va~]) GetType(H,l1) = "function" va !< {null,#undefined} ------------------------------------------------------------ [N-FPcall] H,l,@FPcall.@Exe(l1,va[,va~]) -> H,l,l1.@Call(va[,va~]) @FPapply,@FPapplyProt = make_native_fun(#FPapply,#FPapplyProt,2) GetType(H,l1) != "function" o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) ------------------------------------------ [N-FPapply-exc] H,l,#FPapply.@Exe(l1,va1,va2) -> H2,l,|l2| GetType(H,l1) = "function" va1 < {null,#undefined} ------------------------------------------------------------ [N-FPapply-global] H,l,#FPapply.@Exe(l1,va1,va2) -> H,l,@ExeFPA(l1,#Global,va2) GetType(H,l1) = "function" va1 !< {null,#undefined} -------------------------------------------------------- [N-FPapply] H,l,@FPapply.@Exe(l1,va1,va2) -> H,l,@ExeFPA(l1,va1,va2) va < {null,#undefined} ----------------------------------------- [N-ExeFPA] H,l,@ExeFPA(l1,l2,va) -> H,l,l1.@Call(l2) va !< {null,#undefined} Type(va) !< Object @arrayFlag !< H(l3) o = new_native_error("",#TypeErrorProt) H4,l4= alloc(H,o) --------------------------------------- [N-ExeFPA-Exc1] H,l,@ExeFPA(l1,l2,va) -> H4,l,|l4| @argumentFlag !< H(l3) @arrayFlag !< H(l3) o = new_native_error("",#TypeErrorProt) H4,l4= alloc(H,o) --------------------------------------- [N-ExeFPA-Exc2] H,l,@ExeFPA(l1,l2,l3) -> H4,l,|l4| @argumentFlag < H(l3) H(l3).length = n+1 H(l3) = {["0":va0{DontEnum},...,"n":van{DontEnum},]...} ------------------------------------------------------- [N-ExeFPA-arg] H,l,@ExeFPA(l1,l2,l3) -> H,l,l1.@Call(l2[,va0,...,van]) @arrayFlag < H(l3) H(l3).length = n+1 H(l3) = {["0":va0{},...,"n":van{},]...} ------------------------------------------------------- [N-ExeFPA-arr] H,l,@ExeFPA(l1,l2,l3) -> H,l,l1.@Call(l2[,va0,...,van])
@String = { @Class: "Function", @Prototype: #FunctionProt, "prototype": #StringProt{DontEnum,DontDelete,Readonly}, @Call: true, @Construct: true, "length": 1{ReadOnly,DontDelete,DontEnum}, "fromCharCode": #SfromCharCode{DontEnum} } H(#String).@Actuals > 0 -------------------------------- [N-String-fun] H,l,#String.@Exe(l1,m) -> H,l,m H(#String).@Actuals = 0 -------------------------------- [N-String-fun-0] H,l,#String.@Exe(l1,m) -> H,l,"" H,l,#String.@Construct() -> H,l,#String.@Construct("") [N-String-constr-empty] o = new_String(m) H1,l1 = alloc(h,o) |m| = n H1(l1."length"=n{DontEnum,DontDelete,Readonly}) = H2 ---------------------------------------------------- [N-String-constr] H,l,#String.@Construct(m) -> H2,l,l1 @SfromCharCode,@SfromCharCodeProt = make_native_funv(#SfromCharCode,#SfromCharCode,1) m = StringFromCharCode(n~) --------------------------------------- [N-fromCharCode] H,l,#SfromCharCode.@Exe(l1,n~) -> H,l,m H,l,#SfromCharCode.@Exe(l1) -> H,l,"" [N-fromCharCode-0] @StringProt = { @Class: "String", @Prototype: #ObjectProt, @Value: "", "constructor": #String{DontEnum}, "toString": #SPtoString{DontEnum}, "valueOf": #SPvalueOf{DontEnum} } @SPtoString,@SPtoStringProt = make_native_fun(#SPtoString,#SPtoStringProt,0) H(l1).@Class != "String" o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) --------------------------------------- [N-SPtoString-Exc] H,l,#SPtoString.@Exe(l1) -> H2,l,|l2| H(l1).@Class = "String" H(l1).@Value = m ------------------------------------- [N-SPtoString] H,l,#SPtoString.@Exe(l1) -> H2,l,m @SPvalueOf,@SPvalueOfProt = make_native_fun(#SPvalueOf,#SPvalueOfProt,0) H(l1).@Class != String o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) --------------------------------------- [N-SPvalueOf-Exc] H,l,#SPvalueOf.@Exe(l1) -> H2,l,|l2| H(l1).@Class = String H(l1).@Value = m --------------------------------- [N-SPvalueOf] H,l,#SPvalueOf.@Exe(l1) -> H2,l,m
@Boolean = new_native_constr(#BooleanProt,1) H,l,#Boolean.@Exe(l1,b) -> H,l,b [N-Boolean-fun] H,l,#Boolean.@Construct() -> H,l,#Boolean.@Construct(false) [N-Boolean-constr-false] o = new_Boolean(b) H1,l1 = alloc(h,o) ------------------------------------- [N-Boolean-constr] H,l,#Boolean.@Construct(b) -> H1,l,l1 @BooleanProt = { @Class: "Boolean", @Prototype: #ObjectProt, @Value: false, "constructor": #Boolean{DontEnum}, "toString": #BPtoString{DontEnum}, "valueOf": #BPvalueOf{DontEnum} } @BPtoString,@BPtoStringProt = make_native_fun(#BPtoString,#BPtoStringProt,0) H(l1).@Class != Boolean o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) --------------------------------------- [N-BPtoString-Exc] H,l,#NPtoString.@Exe(l1) -> H2,l,|l2| H(l1).@Class = Boolean H(l1).@Value = b ------------------------------------ [N-BPtoString] H,l,#BPtoString.@Exe(l1) -> H2,l,"b" @BPvalueOf,@BPvalueOfProt = make_native_fun(#BPvalueOf,#BPvalueOfProt,0) H(l1).@Class != Boolean o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) --------------------------------------- [N-BPvalueOf-Exc] H,l,#BPvalueOf.@Exe(l1) -> H2,l,|l2| H(l1).@Class = Boolean H(l1).@Value = b --------------------------------- [N-BPvalueOf] H,l,#BPvalueOf.@Exe(l1) -> H2,l,b
@Number = { @Class: "Function", @Prototype: #FunctionProt, "prototype": #NumberProt{DontEnum,DontDelete,Readonly}, @Call: true, @Construct: true, "length": 1{ReadOnly,DontDelete,DontEnum}, "NaN": &NaN{DontEnum,DontDelete,Readonly} } H(#Number).@Actuals != 0 ------------------------------- [N-Number-fun] H,l,#Number.@Exe(l1,n) -> H,l,n H(#Number).@Actuals = 0 ------------------------------- [N-Number-fun-0] H,l,#Number.@Exe(l1,n) -> H,l,0 H,l,#Number.@Construct() -> H,l,#Number.@Construct(0) [N-Number-constr-0] o = new_Number(n) H1,l1 = alloc(h,o) ------------------------------------ [N-Number-constr] H,l,#Number.@Construct(n) -> H1,l,l1 @NumberProt = { @Class: "Number", @Prototype: #ObjectProt, @Value: 0, "constructor": #Number{DontEnum}, "toString": #NPtoString{DontEnum}, "valueOf": #NPvalueOf{DontEnum} } @NPtoString,@NPtoStringProt = make_native_fun(#NPtoString,#NPtoStringProt,1) H(l1).@Class != Number o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) ---------------------------------------- [N-NPtoString-Exc1] H,l,#NPtoString.@Exe(l1,va) -> H2,l,|l2| H(l1).@Class = Number va !< {&undefined,2,3,...,35,36} o = new_Error() H2,l2= alloc(H,o) ---------------------------------------- [N-NPtoString-Exc2] H,l,#NPtoString.@Exe(l1,va) -> H2,l,|l2| H(l1).@Class = Number pv < {&undefined,10} ------------------------------------------- [N-NPtoString] H,l,#NPtoString.@Exe(l1,pv) -> H2,l,@TS(pv) H(l1).@Class = Number n < {2,3,...,9,11,...,36} ---------------------------------------------------------- [N-NPtoString-ID] H,l,#NPtoString.@Exe(l1,n) -> H2,l,&ImplementationDependent @NPvalueOf,@NPvalueOfProt = make_native_fun(#NPvalueOf,#NPvalueOfProt,0) H(l1).@Class != Number o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) --------------------------------------- [N-NPvalueOf-Exc] H,l,#NPvalueOf.@Exe(l1) -> H2,l,|l2| H(l1).@Class = Number H(l1).@Value = n --------------------------------- [N-NPvalueOf] H,l,#NPvalueOf.@Exe(l1) -> H2,l,n
@Array = { @Class: "Function", @Prototype: #FunctionProt, "prototype": #ArrayProt{DontEnum,DontDelete,Readonly}, @Call: true, @Construct: true, @arrayFlag: true, "length": 1{ReadOnly,DontDelete,DontEnum} } H,l,#Array.@Exe(l1[,va~]) -> H,l,#Array.@Construct([va~]) [N-Array-fun] H(#Array).@Actuals != 1 o = new_Array(n[,va~]) H1,l1 = alloc(h,o) |[va~]| = n --------------------------------------- [N-Array-constr] H,l,#Array.@Construct([va~]) -> H1,l,l1 Type(va) != Number o = new_Array(1,va) H1,l1 = alloc(h,o) ------------------------------------ [N-Array-constr-one] H,l,#Array.@Construct(va) -> H1,l,l1 Type(n) = Number ToUint32(n)=n o = new_Array(n) H1,l1 = alloc(h,o) ----------------------------------- [N-Array-constr-empty] H,l,#Array.@Construct(n) -> H1,l,l1 Type(n) = Number ToUint32(n) != n o = new_native_error("",#RangeErrorProt) H1,l1 = alloc(h,o) ---------------------------------------- [N-Array-constr-Exc] H,l,#Array.@Construct(n) -> H1,l,|l1| @ArrayProt = { @Class: "Array", @Prototype: #ObjectProt, "length": n{DontEnum,DontDelete} "constructor": #Array{DontEnum}, "toString": #APtoString{DontEnum} } H(l1).@Class = "Array" !(H,l1.@CanPut(m)) --------------------------- H,l,l1.@Put(m,va) -> H,l,va H(l1).@Class = "Array" H,l1.@CanPut(m) m !< H(l1) H(l1.m=va{})=H1 !IsArrayIndex(m) ---------------------------- H,l,l1.@Put(m,va) -> H1,l,va H(l1).@Class = "Array" H,l1.@CanPut(m) H(l1):m={[a~]} H(l1.m=va{[a~]}) = H1 !IsArrayIndex(m) ---------------------------- H,l,l1.@Put(m,va) -> H1,l,va H(l1).@Class = "Array" H,l1.@CanPut(m) m !< H(l1) H(l1.m=va{})=H1 ToUint32(m) < H(l1)."length" ---------------------------- H,l,l1.@Put(m,va) -> H1,l,va H(l1).@Class = "Array" H,l1.@CanPut(m) H(l1):m={[a~]} H(l1.m=va{[a~]}) = H1 ToUint32(m) < H(l1)."length" ---------------------------- H,l,l1.@Put(m,va) -> H1,l,va H(l1).@Class = "Array" H,l1.@CanPut(m) m !< H(l1) H(l1.m=va{})=H1 ToUint32(m)=n n >= H(l1)."length" H1(l1."length"=n{DontDelete,DontEnum})=H2 ---------------------------------------- H,l,l1.@Put(m,va) -> H2,l,n H(l1).@Class = "Array" H,l1.@CanPut(m) H(l1):m={[a~]} H(l1.m=va{[a~]}) = H1 ToUint32(m) = n n >= H(l1)."length" H1(l1."length"=n{DontDelete,DontEnum})=H2 ---------------------------------------- H,l,l1.@Put(m,va) -> H2,l,n H(l1).@Class = "Array" H,l1.@CanPut("length") ToUint32(va) = n ToNumber(va) != n ---------------------------------------------- H,l,l1.@Put("length",va) -> H,l,@PutLen(l1,va) ToUint32(n) != n o = new_native_error("",#RangeErrorProt) H2,l2= alloc(H,o) ---------------------------------------- H,l,@PutLen(l1,n) -> H2,l,|l2| ToUint32(n) = n H(l1)."length" = n1 n >= n1 H(l1."length"=n{DontDelete,DontEnum})=H1 ---------------------------------------- H,l,@PutLen(l1,n) -> H1,l,n ToUint32(n) = n H(l1)."length" = n1 n < n1 Expunge(n,n1,H,l1) = H1 H1(l1."length"=n{DontDelete,DontEnum})=H2 ---------------------------------------- H,l,@PutLen(l1,n) -> H2,l,n "n" < H(l) delete(H,l,"n") = H1 --------------------------------------- Expunge(n,n1,H,l) = Expunge(n+1,n1,H,l) Expunge(n,n,H,l) = H
@Error = new_native_constr(#ErrorProt,1) H(#Error).@Actuals = 0 --------------------------------------------------------- [N-String-fun-0] H,l,#Error.@Exe(l1,&undefined) -> H,l,#Error.@Construct() H(#Error).@Actuals != 0 --------------------------------------------------- [N-String-fun] H,l,#Error.@Exe(l1,va) -> H,l,#Error.@Construct(va) H,l,#Error.@Construct() -> H,l,#Error.@Construct("") [N-Error-constr-false] o = new_object("Error",#ErrorProt) H1,l1 = alloc(h,o) H1(l1."message"=m{}) = H2 ----------------------------------- [N-Error-constr] H,l,#Error.@Construct(m) -> H2,l,l1 @ErrorProt = { @Class: "Error", @Prototype: #ObjectProt, "constructor": #Error{DontEnum}, "toString": #EPtoString{DontEnum}, "name": "Error"{}, "message": &ImplementationDependent } @EPtoString,@EPtoStringProt = make_native_fun(#EPtoString,#EPtoStringProt,0) H,l,#EPtoString.@Exe(l1) -> H,l,&ImplementationDependent [N-BPtoString] % Native Errors @NativeError = new_native_constr(#NativeErrorProt,1) H(#NativeError).@Actuals = 0 --------------------------------------------------------------------- [N-String-fun-0] H,l,#NativeError.@Exe(l1,&undefined) -> H,l,#NativeError.@Construct() H(#NativeError).@Actuals != 0 --------------------------------------------------------------- [N-String-fun] H,l,#NativeError.@Exe(l1,va) -> H,l,#NativeError.@Construct(va) H,l,#NativeError.@Construct() -> H,l,#NativeError.@Construct("") [N-NativeError-constr-false] o = new_native_error(m,#NativeErrorProt) H1,l1 = alloc(h,o) ------------------------------------------- [N-NativeError-constr] H,l,#NativeError.@Construct(m) -> H1,l,|l1| @NativeErrorProt = { @Class: "Error", @Prototype: #ErrorProt, "constructor": #NativeError{DontEnum}, "name": "NativeError"{}, "message": &ImplementationDependent }
H(-) = - #Global = @Global #Function = @Function #FunctionProt = @FunctionProt #Object = @Object #ObjectProt = @ObjectProt #Error = @Error #ErrorProt = @ErrorProt #NativeError = @NativeError #NativeErrorProt = @NativeErrorProt #Boolean = @Boolean #BooleanProt = @BooleanProt #Number = @Number #NumberProt = @NumberProt #String = @String #StringProt = @StringProt #GEval = @GEval #GEvalProt = @GEvalProt #isNaN = @isNaN #isNaNProt = @isNaNProt #OPtoString = @OPtoString #OPtoStringProt = @OPtoStringProt ... % and so on and so forth NativeConstructors = { #Function, ... } NativeFunctions = { #GEval, #Function, ... } NativeObjects = { #Object, #GEval, #Function, ... } VariableLen = { #Array, #Function, #FPcall, #SfromCharCode, ... }
new_native_fun(l,n) = { @Class: "Function", @Prototype: #FunctionProt, "prototype": l{DontDelete}, @Call: true, @Construct: true, "length": n{ReadOnly,DontDelete,DontEnum} } make_native_fun(l1,l2,n) = (new_native_fun(l2,n),new_proto("Object",#ObjectProt,l1{DontEnum})) new_native_constr(l,n) = { @Class: "Function", @Prototype: #FunctionProt, "prototype": l{DontEnum,DontDelete,Readonly}, @Call: true, @Construct: true, "length": n{ReadOnly,DontDelete,DontEnum} } make_native_constr(l1,l2,n) = (new_native_constr(l2,n),new_proto("Object",#ObjectProt,l1{DontEnum})) new_Array(n[,va~]) = { ["0": va1{}, ... "n-1": van{},] @Class: "Array", @Prototype: #ArrayProt, "length": n{DontEnum,DontDelete} } new_Boolean(b)= { @Prototype: #BooleanProt, @Class: "Boolean", @Value: b } new_Number(n)= { @Prototype: #NumberProt, @Class: "Number", @Value: n } new_String(m)= { @Prototype: #StringProt, @Class: "String", @Value: m } new_native_error(m,l) = { @Class: "Error", @Prototype: l, "message": m{} }