# Conventions¶

WebAssembly is a programming language that has multiple concrete representations
(its binary format and the text format).
Both map to a common structure.
For conciseness, this structure is described in the form of an *abstract syntax*.
All parts of this specification are defined in terms of this abstract syntax.

## Grammar Notation¶

The following conventions are adopted in defining grammar rules for abstract syntax.

- Terminal symbols (atoms) are written in sans-serif font: \(\mathsf{i32}, \mathsf{end}\).
- Nonterminal symbols are written in italic font: \(\mathit{valtype}, \mathit{instr}\).
- \(A^n\) is a sequence of \(n\geq 0\) iterations of \(A\).
- \(A^\ast\) is a possibly empty sequence of iterations of \(A\). (This is a shorthand for \(A^n\) used where \(n\) is not relevant.)
- \(A^+\) is a non-empty sequence of iterations of \(A\). (This is a shorthand for \(A^n\) where \(n \geq 1\).)
- \(A^?\) is an optional occurrence of \(A\). (This is a shorthand for \(A^n\) where \(n \leq 1\).)
- Productions are written \(\mathit{sym} ::= A_1 ~|~ \dots ~|~ A_n\).
- Large productions may be split into multiple definitions, indicated by ending the first one with explicit ellipses, \(\mathit{sym} ::= A_1 ~|~ \dots\), and starting continuations with ellipses, \(\mathit{sym} ::= \dots ~|~ A_2\).
- Some productions are augmented with side conditions in parentheses, “\((\mathrel{\mbox{if}} \mathit{condition})\)”, that provide a shorthand for a combinatorial expansion of the production into many separate cases.

## Auxiliary Notation¶

When dealing with syntactic constructs the following notation is also used:

- \(\epsilon\) denotes the empty sequence.
- \(|s|\) denotes the length of a sequence \(s\).
- \(s[i]\) denotes the \(i\)-th element of a sequence \(s\), starting from \(0\).
- \(s[i \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} n]\) denotes the sub-sequence \(s[i]~\dots~s[i+n-1]\) of a sequence \(s\).
- \(s \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} [i] = A\) denotes the same sequence as \(s\), except that the \(i\)-the element is replaced with \(A\).
- \(s \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} [i \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} n] = A^n\) denotes the same sequence as \(s\), except that the sub-sequence \(s[i \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} n]\) is replaced with \(A^n\).
- \(\href{../syntax/conventions.html#notation-concat}{\mathrm{concat}}(s^\ast)\) denotes the flat sequence formed by concatenating all sequences \(s_i\) in \(s^\ast\).

Moreover, the following conventions are employed:

- The notation \(x^n\), where \(x\) is a non-terminal symbol, is treated as a meta variable ranging over respective sequences of \(x\) (similarly for \(x^\ast\), \(x^+\), \(x^?\)).
- When given a sequence \(x^n\), then the occurrences of \(x\) in a sequence written \((A_1~x~A_2)^n\) are assumed to be in point-wise correspondence with \(x^n\) (similarly for \(x^\ast\), \(x^+\), \(x^?\)). This implicitly expresses a form of mapping syntactic constructions over a sequence.

Productions of the following form are interpreted as *records* that map a fixed set of fields \(\mathsf{field}_i\) to “values” \(A_i\), respectively:

The following notation is adopted for manipulating such records:

\(r.\mathsf{field}\) denotes the contents of the \(\mathsf{field}\) component of \(r\).

\(r \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \mathsf{field} = A\) denotes the same record as \(r\), except that the contents of the \(\mathsf{field}\) component is replaced with \(A\).

\(r_1 \href{../syntax/conventions.html#notation-compose}{\oplus} r_2\) denotes the composition of two records with the same fields of sequences by appending each sequence point-wise:

\[\{ \mathsf{field}_1\,A_1^\ast, \mathsf{field}_2\,A_2^\ast, \dots \} \href{../syntax/conventions.html#notation-compose}{\oplus} \{ \mathsf{field}_1\,B_1^\ast, \mathsf{field}_2\,B_2^\ast, \dots \} = \{ \mathsf{field}_1\,A_1^\ast~B_1^\ast, \mathsf{field}_2\,A_2^\ast~B_2^\ast, \dots \}\]\(\href{../syntax/conventions.html#notation-compose}{\bigoplus} r^\ast\) denotes the composition of a sequence of records, respectively; if the sequence is empty, then all fields of the resulting record are empty.

The update notation for sequences and records generalizes recursively to nested components accessed by “paths” \(\mathit{pth} ::= ([\dots] \;| \;.\mathsf{field})^+\):

- \(s \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} [i]\,\mathit{pth} = A\) is short for \(s \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} [i] = (s[i] \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \mathit{pth} = A)\).
- \(r \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \mathsf{field}\,\mathit{pth} = A\) is short for \(r \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \mathsf{field} = (r.\mathsf{field} \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \mathit{pth} = A)\).

where \(r \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}}~.\mathsf{field} = A\) is shortened to \(r \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \mathsf{field} = A\).

## Vectors¶

*Vectors* are bounded sequences of the form \(A^n\) (or \(A^\ast\)),
where the \(A\) can either be values or complex constructions.
A vector can have at most \(2^{32}-1\) elements.