An Operational Semantics for JavaScript
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]
Syntax
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
@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}
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+]) % 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
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,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)~}
Scope and Prototype Lookup
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]
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,l3) = {
@Scope: l3,
@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
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
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)
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
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"
!(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
User Expressions
% 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]
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,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]
Statements
% 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}]
Contextual rules for Statements
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
Programs
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]
Native Objects
Global
@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
@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(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])
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"
!(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
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{}
}