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 (email).

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{}
	}