Modules¶

Indices¶

Indices can be given either in raw numeric form or as symbolic identifiers when bound by a respective construct. Such identifiers are looked up in the suitable space of the identifier context $I$ .

\begin{array}{r} \begin{array}{llcllllllll} {typeidx}_{I} & ::= & x : u 32 & \Rightarrow & x \\ | & v : id & \Rightarrow & x & (if I . types [x] = v) \\ {funcidx}_{I} & ::= & x : u 32 & \Rightarrow & x \\ | & v : id & \Rightarrow & x & (if I . funcs [x] = v) \\ {tableidx}_{I} & ::= & x : u 32 & \Rightarrow & x \\ | & v : id & \Rightarrow & x & (if I . tables [x] = v) \\ {memidx}_{I} & ::= & x : u 32 & \Rightarrow & x \\ | & v : id & \Rightarrow & x & (if I . mems [x] = v) \\ {globalidx}_{I} & ::= & x : u 32 & \Rightarrow & x \\ | & v : id & \Rightarrow & x & (if I . globals [x] = v) \\ {elemidx}_{I} & ::= & x : u 32 & \Rightarrow & x \\ | & v : id & \Rightarrow & x & (if I . elem [x] = v) \\ {dataidx}_{I} & ::= & x : u 32 & \Rightarrow & x \\ | & v : id & \Rightarrow & x & (if I . data [x] = v) \\ {localidx}_{I} & ::= & x : u 32 & \Rightarrow & x \\ | & v : id & \Rightarrow & x & (if I . locals [x] = v) \\ {labelidx}_{I} & ::= & l : u 32 & \Rightarrow & l \\ | & v : id & \Rightarrow & l & (if I . labels [l] = v) \end{array} \end{array}

Types¶

Type definitions can bind a symbolic type identifier.

\begin{array}{r} \begin{array}{llclll} type & ::= & ‘ (’ ‘ type ’ {id}^{?} ft : functype ‘) ’ & \Rightarrow & ft \end{array} \end{array}

Type Uses¶

A type use is a reference to a type definition. It may optionally be augmented by explicit inlined parameter and result declarations. That allows binding symbolic identifiers to name the local indices of parameters. If inline declarations are given, then their types must match the referenced function type.

\begin{array}{r} \begin{array}{llcllll} {typeuse}_{I} & ::= & ‘ (’ ‘ type ’ x : {typeidx}_{I} ‘) ’ \Rightarrow x, I^{'} \\ (if \begin{matrix} I . typedefs [x] = [t_{1}^{n}] \to [t_{2}^{*}] \land I^{'} = {locals (ϵ)^{n}}) \end{matrix} \\ | & ‘ (’ ‘ type ’ x : {typeidx}_{I} ‘) ’ (t_{1} : param)^{*} (t_{2} : result)^{*} \Rightarrow x, I^{'} \\ (if \begin{matrix} I . typedefs [x] = [t_{1}^{*}] \to [t_{2}^{*}] \land I^{'} = {locals id (param)^{*}} well-formed) \end{matrix} \end{array} \end{array}

The synthesized attribute of a $typeuse$ is a pair consisting of both the used type index and the local identifier context containing possible parameter identifiers. The following auxiliary function extracts optional identifiers from parameters:

\begin{array}{r} \begin{array}{lcll} id (‘ (’ ‘ param ’ {id}^{?} \dots ‘) ’) & = & {id}^{?} \end{array} \end{array}

Note

Both productions overlap for the case that the function type is $[] \to []$ . However, in that case, they also produce the same results, so that the choice is immaterial.

The well-formedness condition on $I^{'}$ ensures that the parameters do not contain duplicate identifiers.

Abbreviations¶

A $typeuse$ may also be replaced entirely by inline parameter and result declarations. In that case, a type index is automatically inserted:

\begin{array}{r} \begin{array}{llclll} (t_{1} : param)^{*} (t_{2} : result)^{*} & \equiv & ‘ (’ ‘ type ’ x ‘) ’ {param}^{*} {result}^{*} \end{array} \end{array}

where $x$ is the smallest existing type index whose definition in the current module is the function type $[t_{1}^{*}] \to [t_{2}^{*}]$ . If no such index exists, then a new type definition of the form

‘ (’ ‘ type ’ ‘ (’ ‘ func ’ {param}^{*} {result}^{*} ‘) ’ ‘) ’

is inserted at the end of the module.

Abbreviations are expanded in the order they appear, such that previously inserted type definitions are reused by consecutive expansions.

Imports¶

The descriptors in imports can bind a symbolic function, table, memory, or global identifier.

\begin{array}{r} \begin{array}{llclll} {import}_{I} & ::= & ‘ (’ ‘ import ’ \mod : name nm : name d : {importdesc}_{I} ‘) ’ \\ \Rightarrow {module \mod, name nm, desc d} \\ {importdesc}_{I} & ::= & ‘ (’ ‘ func ’ {id}^{?} x, I^{'} : {typeuse}_{I} ‘) ’ & \Rightarrow & func x \\ | & ‘ (’ ‘ table ’ {id}^{?} tt : tabletype ‘) ’ & \Rightarrow & table tt \\ | & ‘ (’ ‘ memory ’ {id}^{?} mt : memtype ‘) ’ & \Rightarrow & mem mt \\ | & ‘ (’ ‘ global ’ {id}^{?} gt : globaltype ‘) ’ & \Rightarrow & global gt \end{array} \end{array}

Abbreviations¶

As an abbreviation, imports may also be specified inline with function, table, memory, or global definitions; see the respective sections.

Functions¶

Function definitions can bind a symbolic function identifier, and local identifiers for its parameters and locals.

\begin{array}{r} \begin{array}{llclll} {func}_{I} & ::= & ‘ (’ ‘ func ’ {id}^{?} x, I^{'} : {typeuse}_{I} (t : local)^{*} (in : {instr}_{I^{″}})^{*} ‘) ’ \\ \Rightarrow {type x, locals t^{*}, body {in}^{*} end} \\ (if I^{″} = I \oplus I^{'} \oplus {locals id (local)^{*}} well-formed) \\ local & ::= & ‘ (’ ‘ local ’ {id}^{?} t : valtype ‘) ’ \Rightarrow t \end{array} \end{array}

The definition of the local identifier context $I^{″}$ uses the following auxiliary function to extract optional identifiers from locals:

\begin{array}{r} \begin{array}{lcll} id (‘ (’ ‘ local ’ {id}^{?} \dots ‘) ’) & = & {id}^{?} \end{array} \end{array}

Note

The well-formedness condition on $I^{″}$ ensures that parameters and locals do not contain duplicate identifiers.

Abbreviations¶

Multiple anonymous locals may be combined into a single declaration:

\begin{array}{r} \begin{array}{llclll} ‘ (’ ‘ local ’ {valtype}^{*} ‘) ’ & \equiv & (‘ (’ ‘ local ’ valtype ‘) ’)^{*} \end{array} \end{array}

Functions can be defined as imports or exports inline:

\begin{array}{r} \begin{array}{llclll} ‘ (’ ‘ func ’ {id}^{?} ‘ (’ ‘ import ’ {name}_{1} {name}_{2} ‘) ’ typeuse ‘) ’ \equiv \\ ‘ (’ ‘ import ’ {name}_{1} {name}_{2} ‘ (’ ‘ func ’ {id}^{?} typeuse ‘) ’ ‘) ’ \\ ‘ (’ ‘ func ’ {id}^{?} ‘ (’ ‘ export ’ name ‘) ’ \dots ‘) ’ \equiv \\ ‘ (’ ‘ export ’ name ‘ (’ ‘ func ’ {id}^{'} ‘) ’ ‘) ’ ‘ (’ ‘ func ’ {id}^{'} \dots ‘) ’ \\ (if {id}^{?} \neq ϵ \land {id}^{'} = {id}^{?} \lor {id}^{?} = ϵ \land {id}^{'} fresh) \end{array} \end{array}

Note

The latter abbreviation can be applied repeatedly, if “ $\dots$ ” contains additional export clauses. Consequently, a function declaration can contain any number of exports, possibly followed by an import.

Tables¶

Table definitions can bind a symbolic table identifier.

\begin{array}{r} \begin{array}{llclll} {table}_{I} & ::= & ‘ (’ ‘ table ’ {id}^{?} tt : tabletype ‘) ’ & \Rightarrow & {type tt} \end{array} \end{array}

Abbreviations¶

An element segment can be given inline with a table definition, in which case its offset is $0$ and the limits of the table type are inferred from the length of the given segment:

\begin{array}{r} \begin{array}{llclll} ‘ (’ ‘ table ’ {id}^{?} reftype ‘ (’ ‘ elem ’ {expr}^{n} : vec (elemexpr) ‘) ’ ‘) ’ \equiv \\ ‘ (’ ‘ table ’ {id}^{'} n n reftype ‘) ’ \\ ‘ (’ ‘ elem ’ ‘ (’ ‘ table ’ {id}^{'} ‘) ’ ‘ (’ ‘ i 32. const ’ ‘ 0 ’ ‘) ’ reftype vec (elemexpr) ‘) ’ \\ (if {id}^{?} \neq ϵ \land {id}^{'} = {id}^{?} \lor {id}^{?} = ϵ \land {id}^{'} fresh) \end{array} \end{array}

\begin{array}{r} \begin{array}{llclll} ‘ (’ ‘ table ’ {id}^{?} reftype ‘ (’ ‘ elem ’ x^{n} : vec (funcidx) ‘) ’ ‘) ’ \equiv \\ ‘ (’ ‘ table ’ {id}^{'} n n reftype ‘) ’ \\ ‘ (’ ‘ elem ’ ‘ (’ ‘ table ’ {id}^{'} ‘) ’ ‘ (’ ‘ i 32. const ’ ‘ 0 ’ ‘) ’ ‘ func ’ vec (funcidx) ‘) ’ \\ (if {id}^{?} \neq ϵ \land {id}^{'} = {id}^{?} \lor {id}^{?} = ϵ \land {id}^{'} fresh) \end{array} \end{array}

Tables can be defined as imports or exports inline:

\begin{array}{r} \begin{array}{llclll} ‘ (’ ‘ table ’ {id}^{?} ‘ (’ ‘ import ’ {name}_{1} {name}_{2} ‘) ’ tabletype ‘) ’ \equiv \\ ‘ (’ ‘ import ’ {name}_{1} {name}_{2} ‘ (’ ‘ table ’ {id}^{?} tabletype ‘) ’ ‘) ’ \\ ‘ (’ ‘ table ’ {id}^{?} ‘ (’ ‘ export ’ name ‘) ’ \dots ‘) ’ \equiv \\ ‘ (’ ‘ export ’ name ‘ (’ ‘ table ’ {id}^{'} ‘) ’ ‘) ’ ‘ (’ ‘ table ’ {id}^{'} \dots ‘) ’ \\ (if {id}^{?} \neq ϵ \land {id}^{'} = {id}^{?} \lor {id}^{?} = ϵ \land {id}^{'} fresh) \end{array} \end{array}

Note

The latter abbreviation can be applied repeatedly, if “ $\dots$ ” contains additional export clauses. Consequently, a table declaration can contain any number of exports, possibly followed by an import.

Memories¶

Memory definitions can bind a symbolic memory identifier.

\begin{array}{r} \begin{array}{llclll} {mem}_{I} & ::= & ‘ (’ ‘ memory ’ {id}^{?} mt : memtype ‘) ’ & \Rightarrow & {type mt} \end{array} \end{array}

Abbreviations¶

A data segment can be given inline with a memory definition, in which case its offset is $0$ and the limits of the memory type are inferred from the length of the data, rounded up to page size:

\begin{array}{r} \begin{array}{llclll} ‘ (’ ‘ memory ’ {id}^{?} ‘ (’ ‘ data ’ b^{n} : datastring ‘) ’ ‘) ’ \equiv \\ ‘ (’ ‘ memory ’ {id}^{'} m m ‘) ’ \\ ‘ (’ ‘ data ’ ‘ (’ ‘ memory ’ {id}^{'} ‘) ’ ‘ (’ ‘ i 32. const ’ ‘ 0 ’ ‘) ’ datastring ‘) ’ \\ (if {id}^{?} \neq ϵ \land {id}^{'} = {id}^{?} \lor {id}^{?} = ϵ \land {id}^{'} fresh, m = ceil (n / 64 Ki)) \end{array} \end{array}

Memories can be defined as imports or exports inline:

\begin{array}{r} \begin{array}{llclll} ‘ (’ ‘ memory ’ {id}^{?} ‘ (’ ‘ import ’ {name}_{1} {name}_{2} ‘) ’ memtype ‘) ’ \equiv \\ ‘ (’ ‘ import ’ {name}_{1} {name}_{2} ‘ (’ ‘ memory ’ {id}^{?} memtype ‘) ’ ‘) ’ \\ ‘ (’ ‘ memory ’ {id}^{?} ‘ (’ ‘ export ’ name ‘) ’ \dots ‘) ’ \equiv \\ ‘ (’ ‘ export ’ name ‘ (’ ‘ memory ’ {id}^{'} ‘) ’ ‘) ’ ‘ (’ ‘ memory ’ {id}^{'} \dots ‘) ’ \\ (if {id}^{?} \neq ϵ \land {id}^{'} = {id}^{?} \lor {id}^{?} = ϵ \land {id}^{'} fresh) \end{array} \end{array}

Note

The latter abbreviation can be applied repeatedly, if “ $\dots$ ” contains additional export clauses. Consequently, a memory declaration can contain any number of exports, possibly followed by an import.

Globals¶

Global definitions can bind a symbolic global identifier.

\begin{array}{r} \begin{array}{llclll} {global}_{I} & ::= & ‘ (’ ‘ global ’ {id}^{?} gt : globaltype e : {expr}_{I} ‘) ’ & \Rightarrow & {type gt, init e} \end{array} \end{array}

Abbreviations¶

Globals can be defined as imports or exports inline:

\begin{array}{r} \begin{array}{llclll} ‘ (’ ‘ global ’ {id}^{?} ‘ (’ ‘ import ’ {name}_{1} {name}_{2} ‘) ’ globaltype ‘) ’ \equiv \\ ‘ (’ ‘ import ’ {name}_{1} {name}_{2} ‘ (’ ‘ global ’ {id}^{?} globaltype ‘) ’ ‘) ’ \\ ‘ (’ ‘ global ’ {id}^{?} ‘ (’ ‘ export ’ name ‘) ’ \dots ‘) ’ \equiv \\ ‘ (’ ‘ export ’ name ‘ (’ ‘ global ’ {id}^{'} ‘) ’ ‘) ’ ‘ (’ ‘ global ’ {id}^{'} \dots ‘) ’ \\ (if {id}^{?} \neq ϵ \land {id}^{'} = {id}^{?} \lor {id}^{?} = ϵ \land {id}^{'} fresh) \end{array} \end{array}

Note

The latter abbreviation can be applied repeatedly, if “ $\dots$ ” contains additional export clauses. Consequently, a global declaration can contain any number of exports, possibly followed by an import.

Exports¶

The syntax for exports mirrors their abstract syntax directly.

\begin{array}{r} \begin{array}{llclll} {export}_{I} & ::= & ‘ (’ ‘ export ’ nm : name d : {exportdesc}_{I} ‘) ’ & \Rightarrow & {name nm, desc d} \\ {exportdesc}_{I} & ::= & ‘ (’ ‘ func ’ x : {funcidx}_{I} ‘) ’ & \Rightarrow & func x \\ | & ‘ (’ ‘ table ’ x : {tableidx}_{I} ‘) ’ & \Rightarrow & table x \\ | & ‘ (’ ‘ memory ’ x : {memidx}_{I} ‘) ’ & \Rightarrow & mem x \\ | & ‘ (’ ‘ global ’ x : {globalidx}_{I} ‘) ’ & \Rightarrow & global x \end{array} \end{array}

Abbreviations¶

As an abbreviation, exports may also be specified inline with function, table, memory, or global definitions; see the respective sections.

Start Function¶

A start function is defined in terms of its index.

\begin{array}{r} \begin{array}{llclll} {start}_{I} & ::= & ‘ (’ ‘ start ’ x : {funcidx}_{I} ‘) ’ & \Rightarrow & {func x} \end{array} \end{array}

Note

At most one start function may occur in a module, which is ensured by a suitable side condition on the $module$ grammar.

Element Segments¶

Element segments allow for an optional table index to identify the table to initialize.

\begin{array}{r} \begin{array}{llclll} {elem}_{I} & ::= & ‘ (’ ‘ elem ’ {id}^{?} (e t, y^{*}) : {elemlist}_{I} ‘) ’ \\ \Rightarrow {type e t, init y^{*}, mode passive} \\ | & ‘ (’ ‘ elem ’ {id}^{?} x : {tableuse}_{I} ‘ (’ ‘ offset ’ e : {expr}_{I} ‘) ’ (e t, y^{*}) : {elemlist}_{I} ‘) ’ \\ \Rightarrow {type e t, init y^{*}, mode active {table x, offset e}} \\ ‘ (’ ‘ elem ’ {id}^{?} ‘ declare ’ (e t, y^{*}) : {elemlist}_{I} ‘) ’ \\ \Rightarrow {type e t, init y^{*}, mode declarative} \\ {elemlist}_{I} & ::= & t : reftype y^{*} : vec ({elemexpr}_{I}) \Rightarrow (type t, init y^{*}) \\ {elemexpr}_{I} & ::= & ‘ (’ ‘ item ’ e : {expr}_{I} ‘) ’ \Rightarrow e \\ {tableuse}_{I} & ::= & ‘ (’ ‘ table ’ x : {tableidx}_{I} ‘) ’ \Rightarrow x \end{array} \end{array}

Abbreviations¶

As an abbreviation, a single instruction may occur in place of the offset of an active element segment or as an element expression:

\begin{array}{r} \begin{array}{llcll} ‘ (’ instr ‘) ’ & \equiv & ‘ (’ ‘ offset ’ instr ‘) ’ \\ ‘ (’ instr ‘) ’ & \equiv & ‘ (’ ‘ item ’ instr ‘) ’ \end{array} \end{array}

Also, the element list may be written as just a sequence of function indices:

\begin{array}{llcll} ‘ func ’ vec ({funcidx}_{I}) & \equiv & ‘ funcref ’ vec (‘ (’ ‘ ref . func ’ {funcidx}_{I} ‘) ’) \end{array}

A table use can be omitted, defaulting to $0$ . Furthermore, for backwards compatibility with earlier versions of WebAssembly, if the table use is omitted, the $‘ func ’$ keyword can be omitted as well.

\begin{array}{r} \begin{array}{llclll} ϵ & \equiv & ‘ (’ ‘ table ’ ‘ 0 ’ ‘) ’ \\ ‘ (’ ‘ elem ’ {id}^{?} ‘ (’ ‘ offset ’ {expr}_{I} ‘) ’ vec ({funcidx}_{I}) ‘) ’ & \equiv & ‘ (’ ‘ elem ’ {id}^{?} ‘ (’ ‘ table ’ ‘ 0 ’ ‘) ’ ‘ (’ ‘ offset ’ {expr}_{I} ‘) ’ ‘ func ’ vec ({funcidx}_{I}) ‘) ’ \end{array} \end{array}

As another abbreviation, element segments may also be specified inline with table definitions; see the respective section.

Data Segments¶

Data segments allow for an optional memory index to identify the memory to initialize. The data is written as a string, which may be split up into a possibly empty sequence of individual string literals.

\begin{array}{r} \begin{array}{llclll} {data}_{I} & ::= & ‘ (’ ‘ data ’ {id}^{?} b^{*} : datastring ‘) ’ \\ \Rightarrow {init b^{*}, mode passive} \\ | & ‘ (’ ‘ data ’ {id}^{?} x : {memuse}_{I} ‘ (’ ‘ offset ’ e : {expr}_{I} ‘) ’ b^{*} : datastring ‘) ’ \\ \Rightarrow {init b^{*}, mode active {memory x^{'}, offset e}} \\ datastring & ::= & (b^{*} : string)^{*} \Rightarrow concat ((b^{*})^{*}) \\ {memuse}_{I} & ::= & ‘ (’ ‘ memory ’ x : {memidx}_{I} ‘) ’ \Rightarrow x \end{array} \end{array}

Note

In the current version of WebAssembly, the only valid memory index is 0 or a symbolic memory identifier resolving to the same value.

Abbreviations¶

As an abbreviation, a single instruction may occur in place of the offset of an active data segment:

\begin{array}{llcll} ‘ (’ instr ‘) ’ & \equiv & ‘ (’ ‘ offset ’ instr ‘) ’ \end{array}

Also, a memory use can be omitted, defaulting to $0$ .

\begin{array}{r} \begin{array}{llclll} ϵ & \equiv & ‘ (’ ‘ memory ’ ‘ 0 ’ ‘) ’ \end{array} \end{array}

As another abbreviation, data segments may also be specified inline with memory definitions; see the respective section.

Modules¶

A module consists of a sequence of fields that can occur in any order. All definitions and their respective bound identifiers scope over the entire module, including the text preceding them.

A module may optionally bind an identifier that names the module. The name serves a documentary role only.

Note

Tools may include the module name in the name section of the binary format.

\begin{array}{r} \begin{array}{lll} module & \begin{array}{cllll} ::= & ‘ (’ ‘ module ’ {id}^{?} (m : {modulefield}_{I})^{*} ‘) ’ \Rightarrow ⨁ m^{*} \\ (if I = ⨁ idc (modulefield)^{*} well-formed) \end{array} \\ {modulefield}_{I} & \begin{array}{clll} ::= & ty : type & \Rightarrow & {types ty} \\ | & im : {import}_{I} & \Rightarrow & {imports im} \\ | & fn : {func}_{I} & \Rightarrow & {funcs fn} \\ | & ta : {table}_{I} & \Rightarrow & {tables ta} \\ | & me : {mem}_{I} & \Rightarrow & {mems me} \\ | & gl : {global}_{I} & \Rightarrow & {globals gl} \\ | & ex : {export}_{I} & \Rightarrow & {exports ex} \\ | & st : {start}_{I} & \Rightarrow & {start st} \\ | & el : {elem}_{I} & \Rightarrow & {elems el} \\ | & da : {data}_{I} & \Rightarrow & {datas da} \end{array} \end{array} \end{array}

The following restrictions are imposed on the composition of modules: $m_{1} \oplus m_{2}$ is defined if and only if

$m_{1} . start = ϵ \lor m_{2} . start = ϵ$
$m_{1} . funcs = m_{1} . tables = m_{1} . mems = m_{1} . globals = ϵ \lor m_{2} . imports = ϵ$

Note

The first condition ensures that there is at most one start function. The second condition enforces that all imports must occur before any regular definition of a function, table, memory, or global, thereby maintaining the ordering of the respective index spaces.

The well-formedness condition on $I$ in the grammar for $module$ ensures that no namespace contains duplicate identifiers.

The definition of the initial identifier context $I$ uses the following auxiliary definition which maps each relevant definition to a singular context with one (possibly empty) identifier:

\begin{array}{r} \begin{array}{lcll} idc (‘ (’ ‘ type ’ {id}^{?} ft : functype ‘) ’) & = & {types ({id}^{?}), typedefs ft} \\ idc (‘ (’ ‘ func ’ {id}^{?} \dots ‘) ’) & = & {funcs ({id}^{?})} \\ idc (‘ (’ ‘ table ’ {id}^{?} \dots ‘) ’) & = & {tables ({id}^{?})} \\ idc (‘ (’ ‘ memory ’ {id}^{?} \dots ‘) ’) & = & {mems ({id}^{?})} \\ idc (‘ (’ ‘ global ’ {id}^{?} \dots ‘) ’) & = & {globals ({id}^{?})} \\ idc (‘ (’ ‘ elem ’ {id}^{?} \dots ‘) ’) & = & {elem ({id}^{?})} \\ idc (‘ (’ ‘ data ’ {id}^{?} \dots ‘) ’) & = & {data ({id}^{?})} \\ idc (‘ (’ ‘ import ’ \dots ‘ (’ ‘ func ’ {id}^{?} \dots ‘) ’ ‘) ’) & = & {funcs ({id}^{?})} \\ idc (‘ (’ ‘ import ’ \dots ‘ (’ ‘ table ’ {id}^{?} \dots ‘) ’ ‘) ’) & = & {tables ({id}^{?})} \\ idc (‘ (’ ‘ import ’ \dots ‘ (’ ‘ memory ’ {id}^{?} \dots ‘) ’ ‘) ’) & = & {mems ({id}^{?})} \\ idc (‘ (’ ‘ import ’ \dots ‘ (’ ‘ global ’ {id}^{?} \dots ‘) ’ ‘) ’) & = & {globals ({id}^{?})} \\ idc (‘ (’ \dots ‘) ’) & = & {} \end{array} \end{array}

Abbreviations¶

In a source file, the toplevel $(module \dots)$ surrounding the module body may be omitted.

\begin{array}{llcll} {modulefield}^{*} & \equiv & ‘ (’ ‘ module ’ {modulefield}^{*} ‘) ’ \end{array}