July 2000 Draft JavaScript 2.0 Formal Description Semantic Notation

Thursday, November 11, 1999

Introduction

To precisely specify the semantics of JavaScript 2.0, we use the notation described below to define the behavior of all JavaScript 2.0 constructs and their interactions.

Semantic Values

The semantics describe the meaning of a JavaScript 2.0 program in terms of operations on simpler objects borrowed from mathematics collectively called semantic values. Semantic values can be held in semantic variables and passed to semantic functions. The kinds of semantic values used in this specification are summarized in the table below and explained in the next few sections:

There is a special semantic value (pronounced as "bottom") that represents the result of an inconsistent or nonterminating computation. Unless specified otherwise, applying any semantic operator (such as +, *, etc.) to or calling a semantic function with as any argument also yields without evaluating any remaining operands or arguments (in technical terms, semantic functions and operators are strict in all of their arguments unless specified otherwise).

If interpreting a JavaScript program according to the semantics here gives a result, an actual implementation executing that JavaScript program will either fail to terminate or throw an exception because it runs out of memory or stack space.

Semantic values of the form value represents the result of a computation that throws a semantic exception. value is the exception's value (which must be a member of the SemanticException semantic type). Unless specified otherwise, applying any semantic operator (such as +, *, etc.) to value or calling a semantic function with value as any argument also yields value (with the same value) without evaluating any remaining operands or arguments.

The throw statement takes a value v and returns v. The catch statement converts v back to v.

Semantic functions that do not return a useful value return the semantic value . There are no operations defined on .

Booleans

The semantic values true and false are booleans. The not, and, or, and xor operators operate on booleans. Like most other operators, and, or, and xor evaluate both operands before returning a result; these operators do not short-circuit.

Integers

Unless specified otherwise, numbers in the semantics written without a slash or decimal point are mathematical integers: ..., -3, -2, -1, 0, 1, 2, 3, .... The usual mathematical operators +, -, *, and unary - can be used on integers. Integers can be compared using =, , <, , >, and .

Rationals

Numbers in the semantics written with a slash are mathematical rational numbers. Every integer is also a rational. Rational numbers include, for example, 0, 1, 2, -1, 1/2, -12/7, and -24/14; the last two are different ways of writing the same rational number. The usual mathematical operators +, -, *, /, and unary - can be used on rationals. Rationals can be compared using =, , <, , >, and .

Doubles

Numbers in the semantics written with a decimal point are double-precision IEEE floating-point numbers (often abbreviated as doubles), including distinct +0.0, -0.0, +, -, and NaN. Doubles are distinct from integers and rationals; when writing doubles in the semantics, we always include a decimal point to distinguish them from integers and rationals.

Doubles other than +, -, and NaN are called finite. We define the significand of a finite double d as follows:

• The significand of +0.0 or -0.0 is 0.
• If d is normalized, we can uniquely represent it as s  m  2^e, where m and e are integers, s  {-1, 1}, 2⁵²  m < 2⁵³, and -1074  e  971. m is the significand.
• If d is denormalized, we can uniquely represent it as s  m  2^-1074, where m is an integer, s  {-1, 1}, and 0 < m < 2⁵². m is the significand.

Characters

Characters are single Unicode 16-bit code points. We write them enclosed in single quotes ‘ and ’. There are exactly 65536 characters: ‘«u0000»’, ‘«u0001»’, ...,‘A’, ‘B’, ‘C’, ..., ‘«uFFFF»’ (see also notation for non-ASCII characters). Unicode surrogates are considered to be pairs of characters for the purpose of this specification.

The characterToCode and codeToCharacter semantic functions convert between characters and their integer Unicode values.

Vectors

A semantic vector contains zero or more elements indexed by integers starting from zero. We write a vector value by enclosing a comma-separated list of values inside bold brackets:

[element0, element1, ... , elementn-1]

For example, the following semantic value is a vector whose elements are four strings:

[“parsley”, “sage”, “rosemary”, “thyme”]

The empty vector is written as [].

Let u = [e0, e1, ... , en-1] and v = [f0, f1, ... , fm-1] be vectors, i and j be integers, and x be a value. The following notations describe common operations on vectors:

Semantic vectors are functional; there is no notation for modifying a semantic vector in place.

Strings

A semantic string is merely a vector of characters. For notational convenience we can write a string literal as zero or more characters enclosed in double quotes. Thus,

“Wonder«LF»”

is equivalent to:

[‘W’, ‘o’, ‘n’, ‘d’, ‘e’, ‘r’, ‘«LF»’]

In addition to all of the other vector operations, we can use =, , <, , >, and to compare two strings.

Sets

A semantic set is an unordered collection of values. Each value may occur at most once in a set. There must be a well-defined = semantic operator defined on all pairs of values in the set, and that operator must induce an equivalence relation.

A semantic set is denoted by enclosing a comma-separated list of values inside braces:

{element1, element2, ... , elementn}

The empty set is written as {}.

For example, the following set contains seven integers:

{3, 0, 10, 11, 12, 13, -5}

When using elements such as integers and characters that have an obvious total order, we can also write sets by using the ... range operator. For example, we can rewrite the above set as:

{0, -5, 3 ... 3, 10 ... 13}

If the beginning of the range is equal to the end of the range, then the range consists of only one element: {7 ... 7} is the same as {7}. If the end of the range is one "less" than the beginning, then the range contains no elements: {7 ... 6} is the same as {}. If the end of the range is more than one "less" than the beginning, then the set is .

Let A and B be sets and x be a value. The following notations describe common operations on sets:

min and max are only defined for sets whose elements can be compared with <.

Tuples

A semantic tuple is an aggregate of several named semantic values. Tuples are sometimes called records or structures in other languages. A tuple is denoted by a comma-separated list of names and values between bold triangular brackets:

name1 value1, name2 value2, ... , namen valuen

Each namei valuei pair is called a field. The order of fields in a tuple is irrelevant, so x 3, y 4 is the same as y 4, x 3. A tuple's names must all be distinct.

Let w be an expression that evaluates to a tuple name1 value1, name2 value2, ... , namen valuen. We can extract the value of the field named namei from w by using the notation w.namei. w is required to have this field. For example, x 3, y 4.x is 3.

In the HTML versions of the semantics, each use of namei is linked back to its tuple type's definition.

Oneofs

A semantic oneof is a pair consisting of a name (called the tag) and a value. Oneofs are sometimes called variants or tagged unions in other languages. A oneof is denoted by writing the tag followed by the value:

name value

For brevity, when value is , we can omit it altogether, so red is the same as red .

Let o be an expression that evaluates to some oneof n v. We can perform the following operations on o:

For example, (red 5) is blue evaluates to false, while (red 5) is red evaluates to true. (red 5).red evaluates to 5.

In addition to the operators above, the case statement evaluates one of several expressions based on a oneof tag.

In the HTML versions of the semantics, each use of name is linked back to its oneof type's definition.

Functions

A semantic function receives zero or more arguments, performs computations, and returns a result. We write a semantic function as follows:

function(param1: type1, ... , paramn: typen) body

Here param1 through paramn are the function's parameters, type1 through typen are the parameters' respective semantic types, and body is an expression that computes the function's result. When the function is called with argument values v1 through vn, the function's body is evaluated and the resulting value returned to the caller. body can refer to the parameters param1 through paramn; each reference to a parameter parami evaluates to the corresponding argument value vi. Arguments are passed by value (which in this language is equivalent to passing them by reference because there is no way to write to a parameter).

Function parameters are statically scoped. When functions are nested and an inner function f defines a parameter with the same name as a parameter of an outer function g, then f's parameter shadows g's parameter inside f.

The only operation allowed on a semantic function f is calling it, which we do using the f(arg1, ..., argn) syntax. In the presence of side effects, f is evaluated first, followed by the argument expressions arg1 through argn, in left-to-right order. If the result of evaluating f or any of the argument expressions is , then the call immediately returns without evaluating the following argument expressions, if any. If the result of evaluating f or any of the argument expressions is v for some value v, then the call immediately returns that v without evaluating the following argument expressions, if any. Otherwise, f's body is evaluated and the resulting value returned to the caller.

Semantic Types

A semantic type is a possibly infinite set of semantic values. Names of semantic types are shown in Capitalized Red Small Caps, and compound semantic type expressions are in red.

We use semantic types to make the semantics more readable by declaring the semantic type of each semantic variable (including function argument variables). Each such declaration states that the only values that will be stored in a semantic variable will be members of that variable's semantic type. These declarations can be proven statically. The JavaScript semantics have been machine type-checked to ensure that every type declaration holds, so, for example, if the semantics state that variable x has type Integer then there does not exist any place that could assign the value true to x.

Semantic type annotations allow us to restrict the description of each semantic operator and function to only describe its behavior on arguments that are members of the arguments' semantic types. Thus, for example, we need not describe the behavior of the + semantic operator when passed the semantic values true and as operands because we can prove that this case cannot arise.

Every semantic type includes the values and v for all values v whose semantic type is SemanticException. For brevity we do not list and v in the tables below.

Basic Semantic Types

The following are the basic semantic types:

The type Rational includes Integer as a subtype because every integer is also a rational number. Except for and v, the types Rational and Double are disjoint.

Compound Semantic Types

We can construct compound semantic types using the notation below. Here t, t1, t2, ..., tn represent some existing semantic types.

The type constructors earlier in the table bind tighter than ones later in the table, so, for example, Integer[]  Rational[] is equivalent to (Integer[])  (Rational[]) (a function that takes a vector of Integers and returns a vector of Rationals) rather than ((Integer[])  Rational)[] (a vector of functions, each of which takes a vector of Integers and returns a Rational). In the rare cases where this is needed, parentheses are used to override precedence.

Semantic Operators

The table below lists the semantic operators in order from the highest precedence (tightest-binding) to the lowest precedence (loosest-binding). Operators under the same heading of the table have the same precedence and associate left-to-right, so, for example, 7-3+2-1 is interpreted as ((7-3)+2)-1 instead of 7-(3+(2-1)) or (7-(3+2))-1. When needed, parentheses can be used to group expressions.

The type signatures of the operators are also listed. Some operators are polymorphic; t, t1, t2, ..., and tn can represent any semantic types. The types of some operators are underdetermined; for example, [] can have type t[] for any type t. In these cases the particular choice of type is inferred from the context.

Each operator in the table below is strict: it evaluates all of its operands left-to-right, and if any operand evaluates to , then the operator immediately returns without evaluating the following operands, if any. If any operand evaluates to v for some value v, then the operator immediately returns that v without evaluating the following operands, if any.

Semantic Statements

Semantic statements are similar to the semantic operators above in that they are also used to construct expressions, take zero or more operands, and return a value. Unlike other semantic operators, semantic statements are usually non-strict: they do not always evaluate all of their operands. Semantic statements have lower precedence than any of the semantic operators above.

Some semantic statements are syntactic sugars, which means that they are defined as macros that expand into other, simpler statements and operators.

Function

function(param1: type1, ... , paramn: typen) body

Let

let var1: type1 = expr1; ... ; varn: typen = exprn in body

Evaluate expr1 through exprn in order and save the results. If any expri evaluates to , then immediately return without evaluating the following expr's. If any expri evaluates to v for some value v, then immediately return that v without evaluating the following expr's. Otherwise evaluate body with new local variable bindings of var1 through varn bound to the saved results of evaluating expr1 through exprn, respectively. Return the result of evaluating body.

type1 through typen are the local variables' respective semantic types. The type of the entire let expression is the type of its body.

The let expression above is syntactic sugar for:

(function(var1: type1, ... , varn: typen) body)(expr1, ... , exprn)

If

if expr then bodytrue else bodyfalse

Evaluate expr. If it evaluates to , then immediately return . If expr evaluates to v for some value v, then immediately return that v. Otherwise expr must evaluate to either true or false. If it evaluated to true, then evaluate bodytrue and return its result. If expr evaluated to false, then evaluate bodyfalse and return its result.

expr must have type Boolean. The entire if expression has any type t such that both bodytrue has type t and bodyfalse has type t.

Case

case expr of
    name1(var1: type1): body1;
    ...
    namen(varn: typen): bodyn;
    end

Evaluate expr. If it evaluates to , then immediately return . If expr evaluates to v for some value v, then immediately return that v. Otherwise expr must evaluate to a oneof name v where name matches namei for some i between 1 and n inclusive. Evaluate the corresponding bodyi with a new local variable vari bound to v. Return bodyi's result.

If we are not interested in using the oneof's value for a particular bodyi, we can shorten that bodyi's clause from:

    namei(vari: typei): bodyi

to:

    namei: bodyi

In this case no local variable is bound while evaluating bodyi.

expr must have type oneof {name1: type1; ... ; namen: typen}. The entire case expression has any type t such that all of its bodyi's have type t. The namei's must be distinct. The order in which the case clauses are listed does not matter.

Throw

throw expr

Evaluate expr. If it evaluates to , then immediately return . If expr evaluates to v for some value v, then immediately return that v. Otherwise expr must evaluate to some value v, in which case return v.

expr must have type SemanticException. The entire throw expression has any type whatsoever (because every semantic type includes v).

Try-Catch

try
    bodytry
catch (var: SemanticException)
    bodyhandler

Evaluate bodytry to obtain a value w. If w does not have the form v for some value v, then return w. Otherwise w is v for some value v. In this case evaluate bodyhandler with a new local variable var bound to v and return bodyhandler's result.

The type of var is always SemanticException. The entire try-catch expression has any type t such that both bodytry has type t and bodyhandler has type t.

Semantic Functions

The sections below list the predefined semantic functions, their type signatures, and short descriptions. All functions are strict and evaluate their arguments left-to-right.

Integer Manipulation

These functions perform bitwise operations on integers. The integers are treated as though they were written in binary notation, with each 1 bit representing true and 0 bit representing false. The integers must be nonnegative.

Double Manipulation

Character Conversions

Character Utilities

The function digitValue is defined as follows:

digitValue(c: Character) : Integer
  = if c  {‘0’ ... ‘9’}
     then characterToCode(c) - characterToCode(‘0’)
     else if c  {‘A’ ... ‘Z’}
     then characterToCode(c) - characterToCode(‘A’) + 10
     else if c  {‘a’ ... ‘z’}
     then characterToCode(c) - characterToCode(‘a’) + 10
     else 

Character Class Queries

Semantic Definitions

Value Definitions

We can define a global semantic constant named var as follows:

var : type = expr

expr should evaluate to a value of type type. expr should not have side effects, and it should not evaluate to .

In the HTML versions of the semantics, each reference to the global semantic constant var is linked to var's definition.

Function Definitions

We can define a global semantic function named f as follows:

f(param1: type1, ... , paramn: typen) : type = body

param1 through paramn are the function's parameters, type1 through typen are the parameters' respective semantic types, type is the function result's semantic type, and body is an expression that computes the function's result.

The above definition is syntactic sugar for the global constant definition:

f : type1  type2  ...  typen  type = function(param1: type1, ... , paramn: typen) body

In the HTML versions of the semantics, each reference to the global semantic function f is linked to f's definition.

For example, the function definition

square(x: Integer) : Integer = x*x

defines a function named square that takes an Integer parameter x and returns an Integer that is the square of x. This is equivalent to the following global definition:

square : Integer  Integer = function(x: Integer) x*x

Type Definitions

We can give a new name to a semantic type t by using the type definition, which has the form:

type name = t

For example, the following notation defines RegExp as a shorthand for tuple {reBody: String; reFlags: String}:

type RegExp = tuple {reBody: String; reFlags: String}

In the HTML versions of the semantics, each reference to the semantic type name name is linked to name's definition.

Semantic Actions

Semantic actions tie together the grammar and the semantics. A semantic action ascribes semantic meaning to a grammar production.

To illustrate the use of semantic actions, we shall look at an example, followed by a detailed description of the notation for specifying semantic actions.

Example

Consider the following grammar, with the start nonterminal Numeral:

This grammar defines the syntax of an acceptable input: “37”, “33#4” and “30#2” are acceptable syntactically, while “1a” is not. However, the grammar does not indicate what these various inputs mean. That is the job of the semantics, which are defined in terms of actions on the parse tree of grammar rule expansions. Consider the following sample set of actions defined on this grammar, with a starting Numeral action called (in this example) Value:

type SemanticException = oneof {syntaxError}

action Value[Digit] : Integer = digitValue(Digit)

action DecimalValue[Digits] : Integer

DecimalValue[Digits  Digit] = Value[Digit]

DecimalValue[Digits  Digits₁ Digit] = 10*DecimalValue[Digits₁] + Value[Digit]

action BaseValue[Digits] : Integer  Integer

BaseValue[Digits  Digit](base: Integer)
  = let d: Integer = Value[Digit]
     in if d < base
         then d
         else throw syntaxError

BaseValue[Digits  Digits₁ Digit](base: Integer)
  = let d: Integer = Value[Digit]
     in if d < base
         then base*BaseValue[Digits₁](base) + d
         else throw syntaxError

action Value[Numeral] : Integer

Value[Numeral  Digits] = DecimalValue[Digits]

Value[Numeral  Digits₁ # Digits₂]
  = let base: Integer = DecimalValue[Digits₂]
     in if base  2 and base  10
         then BaseValue[Digits₁](base)
         else throw syntaxError

Action names are written in violet cursive type. The last action definition states in the example above that the action Value can be applied to any expansion of the nonterminal Numeral, and the result is an Integer. This action maps all acceptable inputs to integers or syntaxError. If the result is syntaxError, then the input satisfies the grammar but contains an error detected by the semantics; this is the case for the input “30#2”. A result of would indicate a nonterminating computation; this cannot happen in this example.

There are two definitions of the Value action on Numeral, one for each grammar production that expands Numeral. Each definition of an action is allowed to call actions on the terminals and nonterminals on the right side of the expansion. For example, Value applied to the first Numeral production (the one that expands Numeral into Digits) simply applies the DecimalValue action to the expansion of the nonterminal Digits and returns the result. On the other hand, Value applied to the second Numeral production (the one that expands Numeral into Digits # Digits) performs a computation using the results of the DecimalValue and BaseValue applied to the two expansions of the Digits nonterminals. In this case there are two identical nonterminals Digits on the right side of the expansion, so we use subscripts to indicate on which one we're calling the actions DecimalValue and BaseValue.

The BaseValue action illustrates a syntactic sugar for defining an action that is a function; this syntactic sugar is analogous to that for defining global functions.

The Value action on Digit illustrates the direct use of a nonterminal in a semantic expression: digitValue(Digit). Here the Digit semantic expression evaluates to the character into which the Digit grammar rule expands.

We can fully evaluate the semantics on our sample inputs to get the following results:

Action Declarations

action Action[nonterminal] : type

This declaration states that action Action is defined on nonterminal nonterminal. Any reference to action Action[nonterminal] in a semantic expression returns a value of type type. The values of action Action must be defined using action definitions for each grammar production that has nonterminal on the left side.

Action Definitions

Action[nonterminal  expansion] = expr

This notation defines the value of action Action on nonterminal nonterminal in the case where nonterminal nonterminal expands to the given expansion. expansion can contain zero or more terminals and nonterminals (as well as other notations allowed on the right side of a grammar production). Furthermore, the terminals and nonterminals of expansion can be subscripted to allow them to be unambiguously referenced by action references or nonterminal references inside expr.

The type of action Action on nonterminal nonterminal must be declared using an action declaration. expr must have the type given by that action declaration.

nonterminal  expansion must be one of the productions in the grammar.

Action Function Definitions

Action[nonterminal  expansion](param1: type1, ... , paramn: typen) = body

This notation is a syntactic sugar for defining an action whose value is a function. This notation is equivalent to:

Action[nonterminal  expansion] =
    function(param1: type1, ... , paramn: typen) body

Combined Action Declarations and Definitions

action Action[nonterminal] : type = expr

This declaration is sometimes used when all expansions of nonterminal nonterminal share the same action semantics. This declaration states both the type type of action Action on nonterminal nonterminal as well as that action's value expr. Note that the expansions are not given between the square brackets, and expr can refer only to the nonterminal nonterminal on the left side of grammar productions. No additional action definitions are needed for nonterminal nonterminal.

See the Value action on Digit in the example above for an example of this declaration.

Waldemar Horwat Last modified Thursday, November 11, 1999