Formal JavaScript Semantics

Thursday, February 8, 2001


The current ECMAScript semantics are written informally and contain many amgibuities and errors. In addition, while experimenting with new language features it is difficult to modify the informal semantics and be assured that the result remains self-consistent and still behaves as expected. In an attempt to remedy these problems, waldemar is writing formal semantics for JavaScript together with an engine that can:


The current semantics cover the lexer and most of expression handling:

Lexer semantics (Word 98 rtf) as a finite-state machine
Expression semantics (Word 98 rtf) as a LR(1) grammar

These are a work in progress. The files are in automatically generated Word RTF format and should be read by Word 97 or 98 (HTML support in current browsers is inadequate to express these). The code that generated and can execute those is in the CVS tree at mozilla/js2/semantics.


There is no documentation (yet) for the notation, but most of it should be self-explanatory.

Type expressions are in red. Integer and Rational represent infinite sets of mathematical integers or rational numbers, respectively.

letexc is a version of let that immediately propagates an exception if it receives one; if it receives a regular value, it works like let.

Grammar syntax

Grammar productions may expand nonterminals into empty right sides. Such right sides are indicated as «empty».

A number of rules in the grammar occur in groups of analogous rules. Rather than list them individually, these groups have been summarized using the shorthand illustrated by the example below:

Statements such as


introduce grammar arguments and . If these arguments later parametrize the nonterminal on the left side of a rule, that rule is implicitly replicated into a set of rules in each of which a grammar argument is consistently substituted by one of its variants. For example,

|  LeftSideExpression = AssignmentExpressionnormal,
|  LeftSideExpression CompoundAssignment AssignmentExpressionnormal,

expands into the following four rules:

|  LeftSideExpressionnormal = AssignmentExpressionnormal,allowIn
|  LeftSideExpressionnormal CompoundAssignment AssignmentExpressionnormal,allowIn
|  LeftSideExpressionnormal = AssignmentExpressionnormal,noIn
|  LeftSideExpressionnormal CompoundAssignment AssignmentExpressionnormal,noIn
|  LeftSideExpressioninitial = AssignmentExpressionnormal,allowIn
|  LeftSideExpressioninitial CompoundAssignment AssignmentExpressionnormal,allowIn
|  LeftSideExpressioninitial = AssignmentExpressionnormal,noIn
|  LeftSideExpressioninitial CompoundAssignment AssignmentExpressionnormal,noIn

AssignmentExpressionnormal,allowIn is now an unparametrized nonterminal and processed normally by the grammar.

Some of the expanded rules (such as the fourth one in the example above) may be unreachable from the starting nonterminal; these are ignored.

Waldemar Horwat
Last modified Thursday, February 8, 2001