C.2 Context-Free Syntax

The grammar in this section uses uppercase words for nonterminal symbols, allowing also hyphens. All other characters stand for themselves, with the following exceptions:

• `::=' and `|' are generally used as meta-notation, as in BNF;
• A string of characters enclosed in double quotation marks `"..."' always stands for the enclosed characters themselves;
• `N t...t N' indicates one or more repetitions of the nonterminal symbol N separated by the terminal symbol t (which is usually a comma or semicolon);
• `N...N' is simply one or more repetitions of N (occasionally, N here is a sequence of terminal and nonterminal symbols, such as `[ SPEC ]');
• `var/vars' indicates that the singular and plural forms may be used interchangeably, and similarly for other keywords; `end/' indicates that the use of `end' is optional, and similarly for semicolons: `;/'.

Context-free parsing of CASL specifications according to the grammar in this section yields a parse tree where terms and formulae occurring in axioms and definitions have been grouped with respect to explicit parentheses and brackets, but where the intended applicative structure has not yet been recognized. A further phase of mixfix grouping analysis is needed, dependent on the symbols declared in the specification and parsing annotations, before the parse tree can be mapped to a complete abstract syntax tree.