4. Lexical Conventions

This chapter presents the lexical conventions of JML, that is, the microsyntax of JML.

Throughout this chapter, grammatical productions are to be understood lexically. That is, no white-space (see section 4.1 White Space) may intervene between the characters of a token. (However, outside this chapter, the opposite of this convention is in force.)

The microsyntax of JML is described by the production microsyntax below; it describes what a program looks like from the point of view of a lexical analyzer [Watt91].

microsyntax ::= lexeme [ lexeme ] ... lexeme ::= white-space | lexical-pragma | comment | annotation-marker | doc-comment | token token ::= ident | keyword | special-symbol | java-literal | informal-description

In the rest of this section we provide more details on each of the major nonterminals used in the above grammar.

4.1 White Space
4.2 Lexical Pragmas
4.3 Comments
4.4 Annotation Markers
4.5 Documentation Comments
4.6 Tokens

4.1 White Space

Blanks, horizontal and vertical tabs, carriage returns, formfeeds, and newlines, collectively called white space, are ignored except as they serve to separate tokens. Newlines and carriage returns are special in that they cannot appear in some contexts where other whitespace can appear, and are also used to end Java-style comments (see section 4.3 Comments).

white-space ::= non-nl-white-space | end-of-line non-nl-white-space ::= a blank, tab, or formfeed character end-of-line ::= newline | carriage-return | carriage-return newline newline ::= a newline character carriage-return ::= a carriage return character

4.2 Lexical Pragmas

ESC/Java [Leino-etal00] has a single kind of "lexical pragma", nowarn, whose syntax is described below in general terms. The JML checker currently ignores these lexical pragmas, but nowarn is only recognized within an annotation. Note that, unlike ESC/Java, the semicolon is mandatory. This restriction seems to be necessary to prevent lexical ambiguity.

lexical-pragma ::= nowarn-pragma nowarn-pragma ::= nowarn [ spaces ] [ nowarn-label-list ] ; spaces ::= non-nl-white-space [ non-nl-white-space ] ... nowarn-label-list ::= nowarn-label [ spaces ] [ , [ spaces ] nowarn-label [ spaces ] ] ... nowarn-label ::= letter [ letter ] ...

See section 4.6 Tokens, for the syntax of letter.

4.3 Comments

Both kinds of Java comments are allowed in JML: multiline C-style comments and single line C++-style comments. However, if what looks like a comment starts with the at-sign (@) character, or with a sequence of annotation-keys and an at-sign (@), then JML considers it to be the start of an annotation (see section 4.4 Annotation Markers), and not a comment. Furthermore, if what looks like a comment starts with an asterisk (*), then it is a documentation comment, which is parsed by JML.

comment ::= C-style-comment | C++-style-comment C-style-comment ::= /* [ C-style-body ] C-style-end C-style-body ::= non-at-plus-minus-star [ non-stars-slash ] ... | + non-letter [ non-stars-slash ] ... | - non-letter [ non-stars-slash ] ... | stars-non-slash [ non-stars-slash ] ... non-letter ::= any character except _, a through z, or A through Z non-stars-slash ::= non-star | stars-non-slash stars-non-slash ::= * [ * ] ... non-star-slash non-at-plus-minus-star ::= any character except @, +, -, or * non-star ::= any character except * non-slash ::= any character except / non-star-slash ::= any character except * or / C-style-end ::= [ * ] ... */ C++-style-comment ::= // [ + ] end-of-line | // non-at-plus-minus-end-of-line [ non-end-of-line ] ... end-of-line | //+ non-letter-end-of-line [ non-end-of-line ] ... end-of-line | //- non-letter-end-of-line [ non-end-of-line ] ... end-of-line non-letter-end-of-line ::= any character except _, a through z, A through Z, a newline, or a carriage return non-end-of-line ::= any character except a newline or carriage return non-at-plus-minus-end-of-line ::= any character except @, +,-, newline, or carriage return non-at-end-of-line ::= any character except @, newline, or carriage return

4.4 Annotation Markers

If what looks to Java like a comment starts with an at-sign (@) as its first character, or starts with a sequence of annotation-keys followed by an at-sign, then it is not considered a comment by JML. We refer to the tokens between //@ and the following end-of-line, and between pairs of annotation start ( /*@ ) and end ( */ or @*/ ) markers as annotations. The definition of an annotation marker is given below.

annotation-marker ::= // [ annotation-key ]... @ [ ignored-at-in-annotation ] ... | /* [ annotation-key ]... @ [ ignored-at-in-annotation ] ... | [ ignored-at-in-annotation ] ... @+*/ | [ ignored-at-in-annotation ] ... */ annotation-key ::= positive-key | negative-key positive-key ::= + ident negative-key ::= - ident ignored-at-in-annotation ::= @

Within annotations, on each line, initial white-space and any immediately following at-signs (@) are ignored.

Note that JML annotations are not the same as Java annotations (see section 6.2.2 Java Annotations). Besides the syntactic differences, JML annotations can appear anywhere a comment may appear, not just attached to declarations.

An annotation-key is a + or - sign followed by an ident (see section 4.6 Tokens). Note that no white space can appear within, before, or after the annotation-key. Tools will provide a way to enable a selection of annotation-key identifiers. These identifiers, hereafter called "keys" provide for conditional inclusion of JML annotations as follows:

• a JML annotation with no keys is always included,
• a JML annotation with at least one positive-key is only included if at least one of these positive keys is enabled and there are no negative-keys in the annotation that have enabled keys, and
• a JML annotation with an enabled negative-key is ignored (even if there are enabled positive-keys).

Annotations must hold entire grammatical units of JML specifications, in the sense that the text of some nonterminals may not be split across two separate annotations. For example the following is illegal, because the postcondition of the ensures clause is split over two annotations, and thus each contains a fragment instead of a complete grammatical unit.

//@ ensures 0 <= x // illegal! //@ && x < a.length;

However, implementations are not required to check for such errors. On the other hand, ESC/Java [Leino-Nelson-Saxe00] and ESC/Java2 assume that nonterminals that define clauses are not split into separate annotations, and so effectively do check for them.

Annotations look like comments to Java, and are thus ignored by it, but they are significant to JML. One way that this can be achieved is by having JML drop (ie., ignore) the character sequences that are annotation-markers, as well as the ignored-at-in-annotations. However, note that this technique does not properly check for annotations that do not contain entire grammatical units of JML specifications, as described in the previous paragraph.

Note that JML will recognize jml-keywords only within JML annotations.

4.5 Documentation Comments

If what looks like a C-style comment starts with an asterisk (*) then it is a documentation comment. The syntax is given below. The syntax doc-comment-ignored is used for documentation comments that are ignored by JML.

doc-comment ::= /** [ * ] ... doc-comment-body [ * ] ... */ doc-comment-ignored ::= doc-comment

At the level of the rest of the JML grammar, a documentation comment that does not contain an embedded JML method specification is essentially described by the above, and the fact that a doc-comment-body cannot contain the two-character sequence */.

However, JML and javadoc both pay attention to the syntax inside of these documentation comments. This syntax is really best described by a context-free syntax that builds on a lexical syntax. However, because much of the documentation is free-form, the context-free syntax has a lexical flavor to it, and is quite line-oriented. Thus it should come as no surprise that the first non-whitespace, non-asterisk (ie., not *) character on a line determines its interpretation.

doc-comment-body ::= [ description ] ... [ tagged-paragraph ] ... [ jml-specs ] [ description ] description ::= doc-non-empty-textline tagged-paragraph ::= paragraph-tag [ doc-non-nl-ws ] ... [ doc-atsign ] ... [ description ] ... jml-specs ::= jml-tag [ method-specification ] end-jml-tag [ jml-tag [ method-specification ] end-jml-tag ] ...

The microsyntax or lexical grammar used within documentation comments is as follows. Note that the token doc-nl-ws can only occur at the end of a line, and is always ignored within documentation comments. Ignoring doc-nl-ws means that any asterisks at the beginning of the next line, even in the part that would be a JML method-specification, are also ignored. Otherwise the lexical syntax within a method-specification is as in the rest of JML. This method specification is attached to the following method or constructor declaration. (Currently there is no useful way to use such specifications in the documentation comments for other declarations.) Note the exception to the grammar of doc-non-empty-textline.

paragraph-tag ::= @author | @deprecated | @exception | @param | @return | @see | @serial | @serialdata | @serialfield | @since | @throws | @version | @ letter [ letter ] ... doc-atsign ::= @ doc-nl-ws ::= end-of-line [ doc-non-nl-ws ] ... [ * [ * ] ... [ doc-non-nl-ws ] ... ] doc-non-nl-ws ::= non-nl-white-space doc-non-empty-textline ::= non-at-end-of-line [ non-end-of-line ] ... jml-tag ::= <jml> | <JML> | <esc> | <ESC> end-jml-tag ::= </jml> | </JML> | </esc> | </ESC>

A jml-tag marks the (temporary) end of a documentation comment and the beginning of text contributing to a method specification. The corresponding end-jml-tag marks the reverse transition. The end-jml-tag must match the corresponding jml-tag.

4.6 Tokens

Character strings that are Java reserved words are made into the token for that reserved word, instead of being made into an ident token. Within an annotation this also applies to jml-keywords. The details are given below.

ident ::= letter [ letter-or-digit ] ... letter ::= _, $, a through z, or A through Z digit ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 letter-or-digit ::= letter | digit

Several strings of characters are recognized as keywords or reserved words in JML. These fall into three separate categories: Java keywords, JML predicate keywords (which start with a backslash), and JML keywords. Java keywords are truly reserved words, and are recognized in all contexts. The nonterminal java-reserved-word represents the reserved words in Java (as in the JDK version supported by the tool in question, hopefully the latest official release).

The jml-keywords are only recognized as keywords when they occur within an annotation, but outside of a spec-expression store-ref-list or constrained-list. JML predicate keywords are also only recognized within annotations, but they are recognized only inside spec-expressions, store-ref-lists, and constrained-lists.

There are options to the JML tools that extend the language in various ways. For example, when an option to parse the syntax for the Universe type system [Dietl-Mueller05] is used, the words listed in the nonterminal java-universe-reserved also act like reserved words in Java (and are thus recognized in all contexts). When an option to recognize the Universe system syntax in annotations is used, these words instead act as jml-keywords and are only recognized in annotations. However, even when no Universe options are used, pure is recognized as a keyword in annotations, since it is also a jml-keyword. (The Universe type system support in JML is experimental. Most likely the list of java-universe-reserved will be added to the list of jml-keywords eventually.)

However, even without the Universe option being on, the jml-universe-pkeyword syntax is recognized within JML annotations in the same way as JML predicate keywords are recognized.

The details are given below.

keyword ::= java-reserved-word | jml-predicate-keyword | jml-keyword java-reserved-word ::= abstract | assert | boolean | break | byte | case | catch | char | class | const | continue | default | do | double | else | extends | false | final | finally | float | for | goto | if | implements | import | instanceof | int | interface | long | native | new | null | package | private | protected | public | return | short | static | strictfp | super | switch | synchronized | this | throw | throws | transient | true | try | void | volatile | while | java-universe-reserved // When the Universe option is on java-universe-reserved ::= peer | pure | readonly | rep jml-predicate-keyword ::= \TYPE | \bigint | \bigint_math | \duration | \elemtype | \everything | \exists | \forall | \fresh | \into | \invariant_for | \is_initialized | \java_math | \lblneg | \lblpos | \lockset | \max | \min | \nonnullelements | \not_assigned | \not_modified | \not_specified | \nothing | \nowarn | \nowarn_op | \num_of | \old | \only_accessed | \only_assigned | \only_called | \only_captured | \pre | \product | \reach | \real | \result | \same | \safe_math | \space | \such_that | \sum | \typeof | \type | \warn_op | \warn | \working_space | jml-universe-pkeyword jml-universe-pkeyword ::= \peer | \readonly | \rep jml-keyword ::= abrupt_behavior | abrupt_behaviour | accessible | accessible_redundantly | also | assert_redundantly | assignable | assignable_redundantly | assume | assume_redundantly | axiom | behavior | behaviour | breaks | breaks_redundantly | callable | callable_redundantly | captures | captures_redundantly | choose | choose_if | code | code_bigint_math | | code_java_math | code_safe_math | constraint | constraint_redundantly | constructor | continues | continues_redundantly | decreases | decreases_redundantly | decreasing | decreasing_redundantly | diverges | diverges_redundantly | duration | duration_redundantly | ensures | ensures_redundantly | example | exceptional_behavior | exceptional_behaviour | exceptional_example | exsures | exsures_redundantly | extract | field | forall | for_example | ghost | helper | hence_by | hence_by_redundantly | implies_that | in | in_redundantly | initializer | initially | instance | invariant | invariant_redundantly | loop_invariant | loop_invariant_redundantly | maintaining | maintaining_redundantly | maps | maps_redundantly | measured_by | measured_by_redundantly | method | model | model_program | modifiable | modifiable_redundantly | modifies | modifies_redundantly | monitored | monitors_for | non_null | normal_behavior | normal_behaviour | normal_example | nowarn | nullable | nullable_by_default | old | or | post | post_redundantly | pre | pre_redundantly | pure | readable | refining | represents | represents_redundantly | requires | requires_redundantly | returns | returns_redundantly | set | signals | signals_only | signals_only_redundantly | signals_redundantly | spec_bigint_math | spec_java_math | spec_protected | spec_public | spec_safe_math | static_initializer | uninitialized | unreachable | when | when_redundantly | working_space | working_space_redundantly | writable | jml-universe-keyword jml-universe-keyword ::= peer | readonly | rep

The following describes the special symbols used in JML. The nonterminal java-special-symbol is the special symbols of Java, taken without change from Java [Gosling-Joy-Steele96].

special-symbol ::= java-special-symbol | jml-special-symbol java-special-symbol ::= java-separator | java-operator java-separator ::= ( | ) | { | } | `[' | `]' | ; | , | . | @ java-operator ::= = | < | > | ! | ~ | ? | : | == | <= | >= | != | && | `||' | ++ | -- | + | - | * | / | & | `|' | ^ | % | << | >> | >>> | += | -= | *= | /= | &= | `|=' | ^= | %= | <<= | >>= | >>>= jml-special-symbol ::= ==> | <== | <==> | <=!=> | -> | <- | <: | .. | `{|' | `|}' | <# | <#=

The nonterminal java-literal represents Java literals which are taken without change from Java [Gosling-Joy-Steele96].

java-literal ::= integer-literal | floating-point-literal | boolean-literal | character-literal | string-literal | null-literal integer-literal ::= decimal-integer-literal | hex-integer-literal | octal-integer-literal decimal-integer-literal ::= non-zero-digit [ digits ] [ integer-type-suffix ] digits ::= digit [ digit ] ... digit ::= 0 | non-zero-digit non-zero-digit ::= 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 integer-type-suffix ::= l | L hex-integer-literal ::= hex-numeral [ integer-type-suffix ] hex-numeral ::= 0x hex-digit [ hex-digit ] ... | 0X hex-digit [ hex-digit ] ... hex-digit ::= digit | a | b | c | d | e | f | A | B | C | D | E | F octal-integer-literal ::= octal-numeral [ integer-type-suffix ] octal-numeral ::= 0 octal-digit [ octal-digit ] ... octal-digit ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 floating-point-literal ::= digits . [ digits ] [ exponent-part ] [ float-type-suffix ] | . digits [ exponent-part ] [ float-type-suffix ] | digits exponent-part [ float-type-suffix ] | digits [ exponent-part ] float-type-suffix exponent-part ::= exponent-indicator signed-integer exponent-indicator ::= e | E signed-integer ::= [ sign ] digits sign ::= + | - float-type-suffix ::= f | F | d | D boolean-literal ::= true | false character-literal ::= ' single-character ' | ' escape-sequence ' single-character ::= any character except ', \, carriage return, or newline escape-sequence ::= \b // backspace | \t // tab | \n // newline | \r // carriage return | \' // single quote | \" // double quote | \\ // backslash | octal-escape | unicode-escape octal-escape ::= \ octal-digit [ octal-digit ] | \ zero-to-three octal-digit octal-digit zero-to-three ::= 0 | 1 | 2 | 3 unicode-escape ::= \u hex-digit hex-digit hex-digit hex-digit string-literal ::= " [ string-character ] ... " string-character ::= escape-sequence | any character except ", \, carriage return, or newline null-literal ::= null

An informal-description looks like (* some text *). It is used in predicates (see section 12.1 Predicates) and in store-ref expressions (see section 12.7 Store Refs) as an escape from formality. The exact syntax is given below.

informal-description ::= (* non-stars-close [ non-stars-close ] ... *) non-stars-close ::= non-star | stars-non-close stars-non-close ::= * [ * ] ... non-star-close non-star-close ::= any character except ) or *