3. Syntax Notation

We use an extended Backus-Naur Form (BNF) grammar to describe the syntax of JML. The extensions are as follows [Ledgard80].

• Nonterminal symbols are written as follows: nonterminal. That is, nonterminal symbols appear in UPPER-CASE (in info files).

• 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.

modifiers ::= [ modifier ] ...

As in the above examples, we follow the C++ standard's conventions [ANSI95] in using nonterminal names of the form X-list to mean a comma-separated list, and nonterminal names of the form X-seq to mean a sequence not separated by commas. An example of a sequence is the following

spec-case-seq ::= spec-case [ also spec-case ] ...

We use "//" to start a comment (to you, the reader) in the grammar.

A complete summary of the JML grammar appears in an appendix (see section C. 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. This is helpful when dealing with such a large grammar.

Another help in dealing with the grammar is to use the index (see section Index). Every nonterminal and terminal symbol in the grammar is found in the index, and each definition and use is noted.