Formal JavaScript Semantics

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:

Status

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.

Notes

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:

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,

AssignmentExpression^,

ConditionalExpression^,

| LeftSideExpression = AssignmentExpression^normal,

| LeftSideExpression CompoundAssignment AssignmentExpression^normal,

AssignmentExpression^{normal,allowIn}

ConditionalExpression^{normal,allowIn}

| LeftSideExpression^normal = AssignmentExpression^{normal,allowIn}

| LeftSideExpression^normal CompoundAssignment AssignmentExpression^{normal,allowIn}

AssignmentExpression^normal,noIn

ConditionalExpression^normal,noIn

| LeftSideExpression^normal = AssignmentExpression^normal,noIn

| LeftSideExpression^normal CompoundAssignment AssignmentExpression^normal,noIn

AssignmentExpression^{initial,allowIn}

ConditionalExpression^{initial,allowIn}

| LeftSideExpression^initial = AssignmentExpression^{normal,allowIn}

| LeftSideExpression^initial CompoundAssignment AssignmentExpression^{normal,allowIn}

AssignmentExpression^initial,noIn

ConditionalExpression^initial,noIn

| LeftSideExpression^initial = AssignmentExpression^normal,noIn

| LeftSideExpression^initial CompoundAssignment AssignmentExpression^normal,noIn

AssignmentExpression^{normal,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.

Introduction

Status

Notes

Grammar syntax