****************************************** Operational Semantics of ECMAScript3 (ES3) ****************************************** Syntactic Conventions and Notation 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 } Values 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 Expressions 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 @AddProps1(e,{[(pn:e)~]}) % GetValue and ToString context, adds properties to a literal object @AddProps2(pn,e,{[(pn:e)~\]}) @AddProps3(e,l,{[(pn:e)~\]}) @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) @GetDefault1(v,v,l) % helper for DefaultValue @GetDefault2(e,v,l) % helper for DefaultValue @GetDefault3(v,l) % helper for DefaultValue @GetDefault4(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} Statements 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,{s*}) % used for blocks @VarList([e,][x[=e]~]) % used for variable declarations @with (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 Programs P ::= % programs fd [P] % function declaration s [P] % statement fd ::= function x "("[x~]"){"[P]"}" % function declaration Types T ::= % Types % public types - primitive Undefined Null Boolean String Number % public types - object Object % internal types Reference Internals Heaps and Objects 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,o) = 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)~} Scope and Prototype Lookup TYPE: Prototype: (H,ln,m)->ln TYPE: Scope: (H,ln,m)->ln %%% Scope Lookup @HasProperty(H,l,m) ------------------- [Scope-ref] Scope(H,L:l,m)=l !(@HasProperty(H,l,m)) -------------------------- [Scope-lookup] Scope(H,L:l,m)=Scope(H,L,m) Scope(H,emp,m)=null [Scope-null] Predefined Object Templates 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) = { @Prototype: null, @IsActivation: true, @this: l2, "arguments": l1{DontDelete} } Internal Properties: Side Effect-Free 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 m < H(l) H(l1).m = va ------------------------ [I-Get] @Get(H,l,m) = va m !< H(l) H(l).@prototype = ln ----------------------------- [I-Get-Proto] @Get(H,l,m) = @Get(H,ln,m) @Get(H,null,m) = &undefined [I-Get-null] m < H(l) ReadOnly < H(l1):m ------------------------------ [I-CanPut-no] @CanPut(H,l,m) = false m < H(l) ReadOnly !< H(l1):m ------------------------------ [I-CanPut-no] @CanPut(H,l,m) = true m !< H(l) H(l).@prototype = ln ----------------------------- [I-CanPut-Proto] @CanPut(H,l,m) = @CanPut(H,ln,m) @CanPut(H,null,m) = true [I-CanPut-null] m < H(l) ---------------------------- H,@HasProperty(H,l,m) = true [I-HasProperty-yes] m !< H(l) H(l).@prototype = ln ------------------------------------------ @HasProperty(H,l,m) = @HasProperty(H,ln,m) [I-HasProperty-proto] H,@HasProperty(H,null,m) = false [I-HasProperty-null] @IsPrototypeOf(H,pv,l2) = false [I-IsPrototypeOf-false] H(l1).@prototype = l2 --------------------------------[I-IsPrototypeOf-true] @IsPrototypeOf(H,l1,l2) = true H(l1).@prototype = l3 l3 != l2 --------------------------------------------------[I-IsPrototypeOf-proto] @IsPrototypeOf(H,l1,l2) = @IsPrototypeOf(H,l3,l2) @IsPrototypeOf(H,null,l2) = false -[I-IsPrototypeOf-null] m !< H(l) ----------------------- [I-Delete-empty] @Delete(H,l,m) = H,true DontDelete < H(l):m ------------------------ [I-Delete-not] @Delete(H,l,m) = H,false DontDelete !< H(l):m del(H,l,m)=H1 ------------------------ [I-Delete-yes] @Delete(H,l,m) = H1,true Helper Functions 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) 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 Types Type Functions 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 Conversions 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| Operational Semantics Internal Properties: Expressions 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" !(@CanPut(H,l1,m)) --------------------------- [I-Put-not] H,L,l1.@Put(m,va) -> H,L,va H(l1).@Class != "Array" @CanPut(H,l1,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" @CanPut(H,l1,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 @Get(H,l1,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,L,l1.@DefaultValue(String) -> H,L,@GetDefault1(l1*"toString", l1*"valueOf",l1) H,L,l1.@DefaultValue([Number]) -> H,L,@GetDefault1(l1*valueOf, l1*"toString",l1) @call < H(l1) -------------------------------------------------------------------- H,L,@GetDefault1(l1,r,l2) -> H,L,@GetDefault2(l1.@Call(l2),r,l2) @call !< H(l1) --------------------------------------------------------------------- H,L,@GetDefault1(l1,r,l2) -> H,L,@GetDefault3(r,l2) H,L,@GetDefault1(pv,r,l2) -> H,L,@GetDefault3(r,l2) H,L,@GetDefault2(pv,r,l2) -> H,L,pv H,L,@GetDefault2(l1,r,l2) -> H,L,@GetDefault3(r,l2) @call < H(l1) -------------------------------------------------------------- H,L,@GetDefault3(l1,l2) -> H,L,@GetDefault4(l1.@call(l2) @call !< H(l) o = new_native_error("",#TypeErrorProt) H3,l3= alloc(H,o) -------------------------------------------------------------- H,L,@GetDefault3(l1,l2) -> H,L,|l3| o = new_native_error("",#TypeErrorProt) H3,l3= alloc(H,o) -------------------------------------------------------------- H,L,@GetDefault3(pv,l2) -> H,L,|l3| H,l,@GetDefault(pv) -> H,l,pv o = new_native_error("",#TypeErrorProt) H3,l3= alloc(H,o) -------------------------------------------------------------- H,L,@GetDefault(l1) -> H,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 new_arguments(n,([va~]),l1) = args alloc(H,args) = H1,l3 H1(l1).@FScope = L1 new_activation(l3,l2) = act alloc(H2,act) = H3,l4 FP(H3,l4,{DontDelete},([x~]),0,n) = H4 VD(H4,l4,{DontDelete},P) = H5 FD(H5,l4,{DontDelete},P) = H6 -------------------------------------------- [I-Call] H,L,l1.@Call(l2[,va~]) -> H6,L1:l4, @FunExe(L,P) H,L,@FunExe(L1,(Throw,va,xe)) -> H,L1,|va| H,L,@FunExe(L1,(Return,va,xe)) -> H,L1,va H,L,@FunExe(L1,(Normal,va,xe)) -> H,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,Ll2 Type(va) != Object ---------------------------------- [I-CCall-v] H,L,@ConstructCall(l1,va) -> H,L,l1 User Expressions % this % Object ScopeThis(H,L,@this) = l H(l).@this=va ----------------------- [E-This] H,L:l,this -> H,L:l,va // Since the global object is the base of every scope chain, Scope @this < H(l) ------------------- [Scope-ref] ScopeThis(H,L:l,m)=l @this !< H(l) -------------------------- [Scope-lookup] ScopeThis(H,L:l,m)=Scope(H,L,m) // Since the global object is the base of every scope chain, // and the global object always has an @this property, the above // recursion always terminates. % identifier % Reference Scope(H,L, idToPname(x))=ln ------------------------------- [E-Ide-val] H,L,x -> H,L,ln*idToPName(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,(@PutValue(l1."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((@PutValye(l1."n",va),l1),n(+)1,([(e|,)~])) [E-AL-init] % Literal object % Object, Exception % @AddProps H,L,{[(pn:e)~]} -> H,L,@AddProps1(new Object(),{[(pn:e)~]}) [E-Obj] H,L,@AddProps1(l,{}) -> H,L,l H,L,@AddProps1(l,{pn1:e1,[(pn:e)~]}) -> H,L,@AddProps2(pn1,e1,l,{[(pn:e)~]}) [E-Obj] H,L,@AddProps2(m,va,l,{[(pn:e)~]}) -> H, L, @AddProps3(@PutValue(l*m,va),l,{[(pn:e)~]})) H,L,@AddProps3(v,l,{[(pn:e)~]}) -> H, L,@AddProps1(l,{[(pn:e)~]}) % H,L,{[(pn:e)~]} -> H,L,@AddProps(new Object(),[,(pn:e)~],0) [E-Obj] % H,L,@AddProps(l,m:va[, (pn:e)~],v) -> H,L,@AddProps(l,[,(pn:e)~],@PutValue(l1.m,va)) [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) H2,Function(fun([x~]){; [P]},L:l1) = H3,l3 H3(l1."x"=l3{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 @Delete(H,l1,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,ypeof 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) @HasInstance(H1,l1,va) = b -------------------------------------------------------- [E-Instof-HasInst] H,L,va instanceof l1 -> H,L,@InstanceOf(l1*"prototype",va) o = new_native_error("",#TypeErrorProt) H2,l2= alloc(H,o) ----------------------------------------- H,L,@InstanceOf(pv,va) -> H2,L,|l2| @IsPrototypeOf(H,va,l) = b ----------------------------------------- H,L,@InstanceOf(l,va) -> H,L,b % 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 @HasProperty(H,l1,m)=b ---------------------- [E-In] H,L,m in l1 -> H,L,b % equality operators: &E < {"==","!=","===","!=="} % Boolean,Exception % @TP, @TN H,L,e1 != e2 -> H,L,!(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] Contextual rules for Expressions H,L,P -> H1,L1,P1 --------------------------- [Ep-Ctx] H,L,eCp[P] -> H1,L1,eCp[P1] eCp ::= @FunExe(l,-) @cEval(-) H,L,e -> H1,L,e1 ------------------------- [E-Ctx] H,L,eC[e] -> H1,L,eC[e1] H,L,eC[w] -> H,L,w [E-Exc] eC ::= (_) % @AddProps(l,[, (pn:e)~],_) @AddProps3(_,l,{[(pn:e)~]}) eCgv _([e~]) delete _ typeof _ - = e - &O"=" e - ++ - "--" ++ - "--" - H,L,eCgv[ln*m] -> H,L,eCgv[@GetValue(ln*m)] [E-GV] eCgv ::= @AddProps1(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~]) @InstanceOf(_,va) @GetDefault1(_,r,l) @GetDefault2(_,r,l) @GetDefault3(_,l) @GetDefault4(_) @ConstructCall(l,_) 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 ::= @AddProps2(-,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 ::= @AddProps1(-,{[(pn:e)~]}) -[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] Statements % Blocks and Statement Lists H,L,{ } -> H,L,(Normal,&empty,&empty) [S-Block-Empty] H,L,{s1[s*]} -> H,L,@Block((Normal,&empty,&empty),s1,{s*}) [S-Block-Start] ct != Normal -------------------------------------------------------------------------------------------------- [S-Block] H,L,@Block((ct1,vae1,xe1),(ct2,vae2,xe2),{s1 [s*]}) -> H,L,(ct2,vae2,xe2) Join(vae1,vae2)=vae -------------------------------------------------------------------------------------------------- [S-Block] H,L,@Block((ct,vae1,xe1),(Normal,vae2,xe2),{s1 [s*]}) -> H,L,@Block((Normal,vae,xe2),s1,{s*}) Join(vae1,vae2)=vae -------------------------------------------------------------------------------------------------- [S-Block] H,L,@Block((ct,vae1,xe1),(Normal,vae2,xe2),{}) -> H,L,(Normal,vae,xe2) %H,L,{s*} -> H,L,@Block1((Normal,&empty,&empty),{s*}) [S-Block-Start] %H,L,@Block1((ct,vae,xe),{}) -> H,L,(ct,vae,xe) [S-Block-End] %H,L,@Block1((ct,vae,xe),{s1[ s*]}) -> H,L,@Block2((ct,vae,xe),s1,{s*}) %ct !< {Normal} %---------------------------------------------- [S-Block-Exc] %H,L,@Block2(co,(ct,vae,xe) s*) -> H,L,(ct,vae,xe) %Join(vae1,vae2)=vae %------------------------------------------------------------------------------- [S-Block] %H,L,@Block2((ct,vae1,xe),(Normal,vae2,xe1),{s*}) -> H,L,@Block1((Normal,vae,xe1),{s*}) %H,L,{ } -> H,L,(Normal,&empty,&empty) [S-Block-Empty] %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 H,L,with (l) s -> H,L:l,@with(s) H,L:l,@with(co) -> H,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}) ---------------------------------------------------------------------------------------- [S-Try-Catch] H,L,try (Throw,va,xe) catch (x) {s1} [finally {s2}] -> H2,L:l1,@catch {s1} [finally {s2}] H,L:l,@catch co [finally {s2}] -> H,L,try co [finally {s2}] Contextual rules for Statements H,L,s -> H1,L1,s1 ------------------------- [S-Ctx] H,L,sC[s] -> H1,L1,sC[s1] sC ::= @Block(co,_,{s*}) @with (l,ln,ln,_) try _ [catch (x) {s1}] [finally {s2}] @catch _ [finally {s2}] try co finally _ @while(e,s,ls,vae,true,_) @sforin(e,ls,s,vae,lo,_,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 Programs H, L, P -> H,L, @Prog(P,{DontDelete}) VD(H,l,{DontDelete},P) = H1 FD(H1,l,{DontDelete},P) = H2 ------------------------------------------- H,L:l,@Prog(P,{a~}) -> H,L:l,@EvalProg(P) H,L,@EvalProg(fd P) -> H,L,@EvalProg((Normal, @empty, @empty) P) ct in {Normal, Return} ----------------------------------------------------- H,L,@EvalProg((ct,vae,xe) P) -> H, L, @EvalProg(P) ct !< {Normal, Return, Throw} o = new_SyntaxError() H1,l1 = alloc(H,o) -------------------------------------------------------- H,L,@EvalProg((ct,vae,xe) P) -> H, L, (Throw,l1,@empty) H,L,@EvalProg((Throw,vae,xe) P) -> H, L, (Throw,vae,xe) //////////////////////////////////////////////////BEGIN DEPRECATION////////////////////////////// VD(H,l,{DontDelete},P) = H1 FD(H,l,{DontDelete},P) = H2 ----------------------------------------- [P-Init] H, L:l, P -> H2,#Global,P 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:l,(Return,vae,xe) P -> H,L:l,(Return,vae,xe) !IsActivation(H,l) o = new_SyntaxError() H1,l1 = alloc(H,o) ----------------------------------------------- [P-Return-Exc] H,L:l,(Return,vae,xe) [P] -> H,L: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] //////////////////////////////////////////////////END DEPRECATION////////////////////////////// H,l,s -> H1,l1,s1 ------------------------- [P-Ctx] H,L,s [P] -> H1,L1,s1 [P] Native Objects Global @Global = { @Prototype: &ImplementationDependent, @Class: &ImplementationDependent, @this: #Global, "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 ----------------------------------------------------- [N-Eval-Global] H,#Global,#GEval.@Exe(l1,m) -> H2,#Global,@cEval(@Prog(P,\{DontDelete\})) l != #Global ParseProg(m) = P ----------------------------------------- [N-Eval-local] H,L:l,#GEval.@Exe(l1,m) -> H2,L:l,@cEval(@Prog(P,{})) ct = Normal Join(&undefined,vae)=v ---------------------------------------- [N-Eval-end] H,L,@cEval((ct,vae,xe)) -> H,L,v ct != Normal ---------------------------------------- [N-Eval-end] H,L,@cEval((ct,vae,xe)) -> H,L,|vae| % 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 @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 Object Prototype @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 @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 Function Prototype @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(va) 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]) Strings @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 Booleans @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 Numbers @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 Arrays @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" !(@CanPut(H,l1,m)) --------------------------- H,L,l1.@Put(m,va) -> H,L,va H(l1).@Class = "Array" @CanPut(H,l1,m) m !< H(l1) H(l1.m=va{})=H1 !IsArrayIndex(m) ---------------------------- H,L,l1.@Put(m,va) -> H1,L,va H(l1).@Class = "Array" @CanPut(H,l1,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" @CanPut(H,l1,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" @CanPut(H,l1,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" @CanPut(H,l1,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" @CanPut(H,l1,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" @CanPut(H,l1,"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 Errors @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 } Reserved Addresses 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, ... } Object Templates 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{} }