2.1 Notations for Grammar

To describe the BML syntax, we use the same grammar conventions as described in Chapter 3 of the JML reference manual. We briefly repeat the most important elements.

We use an extended Backus-Nauer Form (BNF) grammar with the following extensions [Ledgard80].

• Nonterminal symbols are written as follows: nonterminal.
• Terminal symbols are written as follows: terminal.
• Square brackets ([ and ]) surround optional text. Note that [ and ] are terminals.
• The notation ... means that the preceding nonterminal or group of optional text can be repeated zero (0) or more times.

For example, the following gives a production for a non-empty list of init-declarators, separated by commas.

     init-declarator-list ::= init-declarator [ , init-declarator ] ...

To remind the reader that the notation `...' means zero or more repetitions, we try to use `...' only following optional text, although, in cases such as the following, the brackets could have been omitted.

A complete summary of the BML grammar appears in an appendix (see Grammar Summary). When reading the HTML version of this appendix, one can click on the names of nonterminals to bring that nonterminal's definition to the top of the browser's window.