This specification defines the N4JS language.
For the specification of the syntax and structure of elements, we use a slightly augmented similar to the grammar language of Xtext Grammar Language.
Similar to [ECMA11a], we define types with properties only for the purpose of explanation and usage within this specification.
We use the Xtext notation style to assign values to meta-properties.
Particularly, we use the Xtext notation for collection (
+=) and boolean (
These properties are written in italics. Enumerations are defined similar to Xtext.
In order to allow the specification of default values, which are often defined by omitting the value, we always define the literal explicitly if it can be defined by the user.
The following lists informally defines the grammar:
Terminals (or terminal strings) are enclosed in single quotes, e.g.,
Rules which contain only terminals used as values for properties are marked with
Values of non-terminals, e.g., other rules, can be assigned to properties. The property name and the assignment are not part of the original syntax and only used for the meta description. E.g.,
- Collection Properties
If a property is a collection, values are added to that list via
- Boolean Properties
Boolean properties are set to false by default, if the value (usually a terminal) is found, the boolean value is set to true. Often, the name of the property is similar to the terminal. E.g.,
Properties of a non-terminal are sometimes listed again below the grammar. In that case, often pseudo properties are introduced which are derived from other properties and which are only used for simplification.
We use the common notation for rules such as type inference rules , that is
is the rule’s premises (e.g., the expression to be inferred), the result of the rule. is an optional condition which may be omitted.
Both parts of the rule may contain multiple expressions, which are concatenated via 'and'.
For example, the following
can be read as
if , , and are all true, then is true as well.
The following judgments (with relation symbols) are used:
in which the left hand side is a declaration or expression, and the right hand side a type. We also use as a function returning the (inferred) type of an expression.
a relation with three arguments: means, that is expected to be a subtype of inside
The following statement, for example, defines transitivity of subtypes (in a simplified manner):
is the context containing (bound) type variables etc., can be read as
Thus, the rule can be read as follows:
if the type B is a subtype of type A in context (i.e. with constraints on type variables specified in ), and if type C is a subtype of B, then C is also a subtype of A in context .
In rules, we sometimes omit the environment if it is not needed. New information is sometimes added to the environment, in particular, substitutions (that is binding type variables to a type). The set of substitutions is written with (theta). If new substitutions are explicitly added to that set, we write ( is substituted with type ). Often, these bindings are computed from a parameterized type reference which declares type arguments which are bound to the type variables of the generic declaration. In this case we simply write , in which is the parameterized type declaration. As these new substitutions must become part of a (newly) created environment, we then usually write . These substitutions are usually omitted.
A variable or other typed element may be associated with three types:
Declared type: the type explicitly specified in the code, e.g.,
var s: string.
Inferred type: the type inferred by the type inferencer, e.g.,
var s = "Hello"infers the type of s to
string. I.e. will be true, or . If an element is annotated with a type ,i.e. it has a declared type, the inferred type will always be the declared type.
Actual type: the actual type of a variable during runtime. This type information is not available at compile time and ignored in this specification.
These types are not type declarations but type references, in fact, as they may be parameterized. For the sake of simplicity, we often omit the suffix to shorten formulas. Consequently, we define the following properties and pseudo properties for typed elements such as variables:
The explicitly declared type, this is usually a real property of the construct. Not all elements allow the specification of a declared type, such as expressions.
- inferredType or
This pseudo property is the inferred type computed by the type inferencer.
A pseudo property for elements with a property. It is similar to the inferred type, i.e.
This section describes some auxiliary functions required for definition of type inference rules later on.
Binding an identifier (variable reference) to a variable declaration (or variable definition) is not part of this specification as this is standard ECMAScript functionality. However, some valid ECMAScript bindings are permitted due to visibility constraints.
Definition: Binding Relation
We define a pseudo relation
which binds a reference, i.e. an identifier, to a declaration (e.g.,variable declaration).
Binding of variable references to declaration is defined by ECMAScript already. Type references only occur in type expressions, how these are handled is explained in Type Expressions.
We usually omit this binding mechanism in most rules and use the reference similarly to the declaration or definition it is bound to. If a variable reference , for example, is bound to a variable declaration , i.e. , we simply write instead of to refer to the type expression (of the variable).
DeclaredType references the type declaration by its simple name that has been imported from a module specifier.
We define the method for declared types as well:
Definition: Binding Relation of Types
We define a pseudo relation
which binds a type reference, i.e. a simple name, to the type declaration.
In some cases we have to merge types, e.g., types of a union type or item types of an array. For that purpose, we define a method as follows.
Definition: Merge Function
We define a pseudo function
The idea of this function is to remove duplicates. For example; if a union type contains two type expressions and , and if , then contains only one element. The order of the elements is lost, however.
In general, we use a pragmatic mixture of pseudo code, predicate logic, and OCL. Within constraints (also within the inference rules), the properties defined in the grammar are used.
In some rules, it is necessary to type the rule variables. Instead of explicitly checking the metatype (via ), we precede the variable with the type, that is: .
Instead of "type casting" elements, often properties are simply accessed. If an element does not define that element, it is either assumed to be false or null by default.
If a property is optional and not set, we write to test its absence. Note that is different from , as the latter refers to the null type. Non-terminals may implicitly be subclasses. In that case, the concrete non-terminal, or type, of a property may be subject for a test in a constraint.
Variables and their properties are printed in italic when used in formulas (such as rules). A dot-notation is used for member access, e.g. . Also defined functions are printed in italic, e.g., . Properties which define sets are usually ordered and we assume 0-indexed access to elements, the index subscripted, e.g., .
We use the following symbols and font conventions:
- , , ,
Logical and, or, exclusive or (xor), and not.
- , , , ,
Logical implication, if and only if, and if-then-else.
- , , ,
Boolean true, boolean false, null (i.e., not specified, e.g., means that there are is no (super class) specified), empty set.
- , , , ,
Element of, not an element of, union set, intersection set, cardinality of set x.
Power set of , i.e. .
- , ,
Exists, not exists, for all; we write and say
"there exists such that predicate is true".
Note that .
(mu) read "metatype of"; metatype of a variable or property, e.g.,
Sequence of elements . E.g., if we want to define a constraint that the owner of a members of a class is the class, we simply write
or even more complicated with index variables.
Sequences are 1-based, e.g., a sequence with length , has elements .