Go to the first, previous, next, last section, table of contents.


B. Syntax

We use an extended BNF grammar to describe the syntax of JML. The extensions are as follows [Ledgard80].

For example, the following gives a production for the nonterminal name, which is a non-empty list of ident's separated by periods (.).

name ::= ident [ . ident ] ...

To remind the reader that the notation `...' means zero or more repetitions, we use `...' only following optional text.

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

B.1 Context-Free Syntax

B.1.1 Compilation Unit Syntax

The following is the syntax of compilation units in JML. The compilation-unit rule is the start rule for the JML grammar.

compilation-unit ::= [ package-definition ]
              [ refine-prefix ]
              [ import-definition ] ...
              [ type-definition ] ...
package-definition ::= package name ;
refine-prefix ::= refine ident-list <- string-literal ;
ident-list ::= ident [ , ident ] ...
import-definition ::= [ model ] import  name-star ;
name ::= ident  [ . ident ] ...
name-star ::= ident [ . ident ] ... [ . * ]

B.1.2 Type Definition Syntax

The following is the syntax of type definitions. The order of the modifier productions suggests the relative order for writing the modifiers in code and specifications, with public before all other modifiers, and non_null last.

type-definition ::= [ doc-comment ] modifiers class-or-interface-def
        | ;
class-or-interface-def ::= class-definition | interface-definition
type-spec ::= type [ dims ] | \TYPE [ dims ]
type ::= reference-type | builtInType
reference-type ::= name
modifiers ::= [ modifier ] ...
modifier ::= public | private | protected
        | spec_public | spec_protected
        | abstract | static |
        | model | ghost | pure
        | final | synchronized
        | instance | helper
        | transient | volatile
        | native | strictfp
        | const | monitored | uninitialized
        | non_null
class-definition ::= class ident [ extends name [ weakly ] ]
              [ implements-clause ] class-block
interface-definition ::= interface ident [ interface-extends ] class-block
interface-extends ::= extends name-weakly-list
implements-clause ::= implements name-weakly-list
name-weakly-list ::= name [ weakly ] [ , name [ weakly ] ] ...
class-block ::= { [ field ] ... }

B.1.3 Field Syntax

The following gives the syntax of fields.

field ::= [ doc-comment ] ... modifiers member-decl
        | modifiers jml-declaration
        | [ method-specification ] [ static ] compound-statement
        | method-specification static_initializer 
        | method-specification initializer 
        | axiom predicate ;
        | ;
member-decl ::= variable-decls ; | method-decl
        | class-definition | interface-definition
variable-decls ::= type-spec variable-declarators [ jml-var-assertion ]
variable-declarators ::= variable-declarator [ , variable-declarator ] ...
variable-declarator ::= ident [ dims ] [ = initializer ]
initializer ::= expression | array-initializer
array-initializer ::= { [ initializer-list ] } 
initializer-list ::= initializer [ , initializer ] ... [ , ]
method-decl ::= method-specification
              [ type-spec ] method-head method-body
        | [ type-spec ] method-head
          [ method-specification ]
          method-body
method-head ::= ident ( [ param-declaration-list ] )
              [ dims ] [ throws-clause ]
method-body ::= compound-statement | ;
throws-clause ::= throws name [ , name ] ...
param-declaration-list ::= param-declaration [ , param-declaration ] ...
param-declaration ::= [ param-modifier ] ... type-spec ident [ dims ]
param-modifier ::= final | non_null

B.1.4 Behavioral Specification Syntax for Types

The following gives the syntax of behavioral specifications for types.

jml-var-assertion ::= initially predicate
        | readable_if predicate
        | monitored_by spec-expression-list
        | monitored
jml-declaration ::= invariant | history-constraint
        | depends-decl | represents-decl
invariant ::= invariant-keyword predicate ;
invariant-keyword ::= invariant | invariant_redundantly
history-constraint ::= constraint-keyword predicate
              [ for constrained-list ] ;
constraint-keyword ::= constraint | constraint_redundantly
constrained-list ::= method-name-list | \everything
method-name-list ::= method-name [ , method-name ] ...
method-name ::= method-ref [ ( [ param-disambig-list ] ) ]
method-ref ::= method-ref-start [ . method-ref-rest ] ...
        | new reference-type
method-ref-start ::=  super | this | ident | \other
method-ref-rest ::=  this | ident | \other
param-disambig-list ::= param-disambig [ , param-disambig ] ...
param-disambig ::= type-spec [ ident [ dims ] ]
depends-decl ::= depends-keyword store-ref-expression <- store-ref-list ;
depends-keyword ::= depends | depends_redundantly
represents-decl ::= represents-keyword
              store-ref-expression <- spec-expression ;
        | represents-keyword
              store-ref-expression \such_that predicate ;
represents-keyword ::= represents | represents_redundantly

B.1.5 Store Ref Syntax

The syntax related to the store-ref production is used in several places.

store-ref-list ::= store-ref [ , store-ref ] ...
store-ref ::= store-ref-expression
        | \fields_of ( spec-expression [ , reference-type [ , store-ref-expression ] ] )
        | informal-description
        | store-ref-keyword
store-ref-expression ::= store-ref-name [ store-ref-name-suffix ] ...
store-ref-name ::= ident | super | this
store-ref-name-suffix ::= . ident | . this | `[' spec-array-ref-expr `]'
spec-array-ref-expr ::= spec-expression
        | spec-expression .. spec-expression
        | *
store-ref-keyword ::= \nothing | \everything | \not_specified | \private_data

B.1.6 Behavioral Specification Syntax for Methods

The following gives the syntax of behavioral specifications for methods. We start with the top-level syntax that organizes these specifications.

method-specification ::= specification | extending-specification
specification ::= spec-case-seq
              [ subclassing-contract ]
              [ redundant-spec ]
        | subclassing-contract
              [ redundant-spec ]
        | redundant-spec
spec-case-seq ::= spec-case [ also spec-case ] ...
spec-case ::= generic-spec-case | behavior-spec | model-program
extending-specification ::= also specification
privacy ::= public | protected | private
exceptional-simple-spec-body ::= exceptional-spec-clause [ exceptional-spec-clause ] ...
exceptional-spec-clause ::= diverges-clause | measured-clause
        | assignable-clause | accessible-clause
        | when-clause | working-space-clause
        | duration-clause | signals-clause
normal-simple-spec-body ::= normal-spec-clause [ normal-spec-clause ] ...
normal-spec-clause ::= diverges-clause | measured-clause
        | assignable-clause | accessible-clause
        | when-clause | working-space-clause
        | duration-clause | ensures-clause
redundant-spec ::= implications [ examples ] | examples
implications ::= implies_that spec-case-seq
examples ::= for_example example [ also example ] ...

The following is the syntax of generic specification cases. These are the least verbose and most general specification cases.

generic-spec-case ::= [ spec-var-decls ] spec-header [ generic-spec-body ]
        | [ spec-var-decls ] generic-spec-body
spec-header ::= requires-clause [ requires-clause ] ...
generic-spec-body ::= simple-spec-body
        | {| generic-spec-case-seq |}
generic-spec-case-seq ::= generic-spec-case [ also generic-spec-case ] ...
simple-spec-body ::= simple-spec-body-clause [ simple-spec-body-clause ] ...
simple-spec-body-clause ::= diverges-clause | measured-clause
        | assignable-clause | accessible-clause
        | when-clause | working-space-clause
        | duration-clause | ensures-clause | signals-clause

The following gives the syntax of specification cases that start with one of the behavior keywords.

behavior-spec ::= [ privacy ] behavior generic-spec-case
        | [ privacy ] exceptional_behavior exceptional-spec-case
        | [ privacy ] normal_behavior normal-spec-case
exceptional-spec-case ::= [ spec-var-decls ] spec-header
                 [ exceptional-spec-body ]
        | [ spec-var-decls ] exceptional-spec-body
exceptional-spec-body ::= exceptional-spec-clause [ exceptional-spec-clause ] ... 
        | {| exceptional-spec-case-seq |}
exceptional-spec-case-seq ::= exceptional-spec-case
             [ also exceptional-spec-case ] ...
normal-spec-case ::= [ spec-var-decls ] spec-header
             [ normal-spec-body ]
        | [ spec-var-decls ] normal-spec-body
normal-spec-body ::= normal-spec-clause [ normal-spec-clause ] ... 
        | {| normal-spec-case-seq |}
normal-spec-case-seq ::= normal-spec-case [ also normal-spec-case ] ...

The following gives the syntax of subclassing contracts.

subclassing-contract ::= subclassing_contract
             accessible-clause [ accessible-clause ] ...
             [ callable-clause ] ...
        | subclassing_contract
             callable-clause [ callable-clause ] ...
accessible-clause ::= accessible-keyword object-ref-list ;
object-ref-list ::= object-ref [ , object-ref ] ...
        | store-ref-keyword
object-ref ::= store-ref-expression
        | \other [ store-ref-name-suffix ] ...
accessible-keyword ::= accessible | accessible_redundantly
callable-clause ::= callable-keyword callable-methods-list ;
callable-keyword ::= callable | callable_redundantly
callable-methods-list ::= method-name-list | store-ref-keyword

B.1.7 Model Program Syntax

The following gives the syntax of model programs, adapted from the refinement calculus [Back88] [Back-vonWright89a] [Morgan94] [Morris87]. See section B.1.11 Statement and Annotation Statement Syntax, for the parts of the syntax of statements that are unchanged from Java. The jml-compound-statement and jml-statement syntax is the same as the compound-statement and statement syntax, except that model-prog-statements are not flagged as errors within the jml-compound-statement and jml-statements.

model-program ::= [ privacy ] model_program jml-compound-statement
jml-compound-statement ::= compound-statement
jml-statement ::= statement
model-prog-statement ::= nondeterministic-choice
        | nondeterministic-if
        | spec-statement
        | invariant
nondeterministic-choice ::= choose alternative-statements
alternative-statements ::= jml-compound-statement
             [ or jml-compound-statement ] ...
nondeterministic-if ::= choose_if guarded-statements
             [ else jml-compound-statement ]
guarded-statements ::= guarded-statement
             [ or guarded-statement ] ...
guarded-statement ::= {
             assume-statement
             jml-statement [ jml-statement] ...
         }

The grammar for specification statements appears below. It is unusual, compared to specification statements in refinement calculus, in that it allows one to specify statements that can signal exceptions, or terminate abruptly. The reasons for this are based on verification logics for Java [Huisman01] [Poll-Jacobs00], which have these possibilities. The meaning of an abrupt-spec-case is that the normal termination and signaling an exception are forbidden; that is, the equivalent spec-statement using behavior would have ensures false; and signals (Exception) false; clauses.

spec-statement ::= [ privacy ] behavior generic-spec-statement-case
        | [ privacy ] exceptional_behavior exceptional-spec-case
        | [ privacy ] normal_behavior normal-spec-case
        | [ privacy ] abrupt_behavior abrupt-spec-case
generic-spec-statement-case ::= [ spec-var-decls ] generic-spec-statement-body
        | [ spec-var-decls ] spec-header [ generic-spec-statement-body ]
generic-spec-statement-body ::= simple-spec-statement-body
        | {| generic-spec-statement-case-seq |}
generic-spec-statement-body-seq ::= generic-spec-statement-case
             [ also generic-spec-statement-case ] ...
simple-spec-statement-body ::= simple-spec-statement-clause
             [ simple-spec-statement-clause ] ... 
simple-spec-statement-clause ::= diverges-clause
        | assignable-clause | accessible-clause
        | when-clause | working-space-clause | duration-clause
        | ensures-clause | signals-clause
        | continues-clause | breaks-clause | returns-clause
abrupt-spec-case ::= [ spec-var-decls ] spec-header
             [ abrupt-spec-body ]
        | [ spec-var-decls ] abrupt-spec-body
abrupt-spec-body ::= abrupt-spec-clause [ abrupt-spec-clause ] ... 
        | {| abrupt-spec-case-seq |}
abrupt-spec-clause ::= diverges-clause
        | assignable-clause | accessible-clause
        | when-clause | working-space-clause | duration-clause
        | continues-clause | breaks-clause | returns-clause
abrupt-spec-case-seq ::= abrupt-spec-case [ also abrupt-spec-case ] ...

continues-clause ::= continues-keyword [ target-label ] [ pred-or-not ] ;
continues-keyword ::= continues | continues_redundantly
target-label ::= -> ( ident )
breaks-clause ::= breaks-keyword [ target-label ] [ pred-or-not ] ;
breaks-keyword ::= breaks | breaks_redundantly
returns-clause ::= returns-keyword [ pred-or-not ] ;
returns-keyword ::= returns | returns_redundantly

B.1.8 Example Syntax

The following gives the syntax of examples.

example ::= [ [ privacy ] example ]
             [ spec-var-decls ] [ spec-header ] simple-spec-body
        | [ privacy ] exceptional_example
             [ spec-var-decls ] spec-header [ exceptional-example-body ]
        | [ privacy ] exceptional_example
             [ spec-var-decls ] exceptional-example-body
        | [ privacy ] normal_example
             [ spec-var-decls ] spec-header [ normal-example-body ]
        | [ privacy ] normal_example
             [ spec-var-decls ] normal-example-body
exceptional-example-body ::= exceptional-spec-clause [ exceptional-spec-clause ] ...
normal-example-body ::= normal-spec-clause [ normal-spec-clause ] ...

B.1.9 Method Specification Clause Syntax

The following gives the syntax of clauses that occur in method specifications.

spec-var-decls ::= forall-var-decls [ old-var-decls ]
        | old-var-decls
forall-var-decls ::= forall-var-decl [ forall-var-decl ] ... 
forall-var-decl ::= forall quantified-var-decl ;
old-var-decls ::= old-var-decl [ old-var-decl ] ...
old-var-decl ::= old type-spec spec-variable-declarators ;
requires-clause ::= requires-keyword pred-or-not ;
requires-keyword ::= requires | pre 
        | requires_redundantly | pre_redundantly
pred-or-not ::= predicate | \not_specified
when-clause ::= when-keyword pred-or-not ;
when-keyword ::= when | when_redundantly
working-space-clause ::= working-space-keyword \not_specified ;
        | working-space-keyword spec-expression [ if predicate ] ;
working-space-keyword ::= working_space | working_space_redundantly
duration-clause ::= duration-keyword \not_specified ;
        | duration-keyword spec-expression [ if predicate ] ;
duration-keyword ::= duration | duration_redundantly
measured-clause ::= measured-by-keyword \not_specified ;
        | measured-by-keyword spec-expression [ if predicate ] ;
measured-by-keyword ::= measured_by | measured_by_redundantly
assignable-clause ::= assignable-keyword conditional-store-ref-list ;
assignable-keyword ::= assignable | assignable_redundantly
        | modifiable | modifiable_redundantly
        | modifies | modifies_redundantly
conditional-store-ref-list ::= conditional-store-ref
             [ , conditional-store-ref ] ... 
conditional-store-ref ::= store-ref [ if predicate ]
ensures-clause ::= ensures-keyword pred-or-not ;
ensures-keyword ::= ensures | post
        | ensures_redundantly | post_redundantly
signals-clause ::= signals-keyword
         ( reference-type [ ident ] ) [ pred-or-not ] ;
signals-keyword ::= signals | signals_redundantly
        | exsures | exsures_redundantly
diverges-clause ::= diverges-keyword pred-or-not ;
diverges-keyword ::= diverges | diverges_redundantly

B.1.10 Predicate and Specification Expression Syntax

The following gives the syntax of predicates and specification expressions. Within a spec-expression, one cannot use any of the operators (such as ++, --, and the assignment operators) that would necessarily cause side effects. See section B.1.12 Expression Syntax, for the syntax of expressions.

predicate ::= spec-expression
spec-expression-list ::= spec-expression [ , spec-expression ] ...
spec-expression ::= expression 

jml-primary ::= \result
        | \old ( spec-expression )
        | \not_modified ( store-ref-list )
        | \fresh ( spec-expression-list )
        | \reach ( spec-expression [ , reference-type [ , store-ref-expression ] ] )
        | \duration ( expression )
        | \space ( spec-expression )
        | \working_space ( expression )
        | informal-description
        | \nonnullelements ( spec-expression )
        | \typeof ( spec-expression )
        | \elemtype ( spec-expression )
        | \type ( type )
        | \lockset
        | \is_initialized ( reference-type )
        | \invariant_for ( spec-expression )
        | ( \lblneg ident spec-expression )
        | ( \lblpos ident spec-expression )
        | spec-quantified-expr

set-comprehension ::= { type-spec quantified-var-declarator 
                         `|' set-comprehension-pred }
set-comprehension-pred ::= postfix-expr . has ( ident ) 
                           && predicate 

spec-quantified-expr ::= ( quantifier quantified-var-decls ; [ [ predicate ] ; ]
                           spec-expression )
quantifier ::= \forall | \exists | \max | \min | \num_of | \product | \sum
quantified-var-decls ::= type-spec quantified-var-declarator
                  [ , quantified-var-declarator ] ...
quantified-var-declarator ::= ident [ dims ]

spec-variable-declarators ::= spec-variable-declarator
                          [ , spec-variable-declarator ] ...
spec-variable-declarator ::= ident [ dims ] [ = spec-initializer ]
spec-array-initializer ::= { [ spec-initializer
             [ , spec-initializer ] ... [ , ] ] }
spec-initializer ::= spec-expression
        | spec-array-initializer

B.1.11 Statement and Annotation Statement Syntax

The following gives the syntax of statements. These are the standard Java statements, with the addition of annotations, the hence-by-statement, assert-redundantly-statement, assume-statement, set-statement, and unreachable-statement, and the various forms of model-prog-statement. See section B.1.7 Model Program Syntax, for the syntax of model-prog-statement, which is only allowed in model programs.

compound-statement ::= { statement [ statement ] ... }
statement ::= compound-statement
        | local-declaration ;
        | ident : statement
        | expression ;
        | if ( expression ) statement [ else statement ]
        | [ loop-invariant ] ... [ variant-function ] ... [ ident : ] loop-stmt
        | break [ ident ] ;
        | continue [ ident ] ;
        | return [ expression ] ;
        | switch-statement
        | try-block 
        | throw expression ;
        | synchronized ( expression ) statement
        | ;
        | assert-statement
        | hence-by-statement
        | assert-redundantly-statement
        | assume-statement
        | set-statement
        | unreachable-statement
        | model-prog-statement // only allowed in model programs
loop-stmt ::= while ( expression ) statement
        | do statement while ( expression ) ;
        | for ( [ for-init ] ; [ expression ] ; [ expression-list ] )
             statement
for-init ::= local-declaration | expression-list
local-declaration ::= local-modifiers variable-decls
local-modifiers ::= [ local-modifier ] ...
local-modifier ::= model | ghost | final | non_null
switch-statement ::= switch ( expression ) { [ switch-body ] ... }
switch-body ::= switch-label-seq [ statement ] ...
switch-label-seq ::= switch-label [ switch-label ] ...
switch-label ::= case expression : | default :
try-block ::= try compound-statement [ handler ] ...
             [ finally compound-statement ]
handler ::= catch ( param-declaration ) compound-statement
assert-statement ::= assert expression [ : expression ] ;

The following gives the syntax of JML annotations that can be used on statements. See section B.1.7 Model Program Syntax, for the syntax of statements that can only be used in model programs.

hence-by-statement ::= hence-by-keyword predicate ;
hence-by-keyword ::= hence_by | hence_by_redundantly
assert-redundantly-statement ::= assert_redundantly predicate [ : expression ] ;
assume-statement ::= assume-keyword predicate [ : expression ] ;
assume-keyword ::= assume | assume_redundantly
set-statement ::= set assignment-expr ;
unreachable-statement ::= unreachable ;
loop-invariant ::= maintaining-keyword predicate ;
maintaining-keyword ::= maintaining | maintaining_redundantly
        | loop_invariant | loop_invariant_redundantly
variant-function ::= decreasing-keyword spec-expression ;
decreasing-keyword ::= decreasing | decreasing_redundantly
        | decreases | decreases_redundantly

B.1.12 Expression Syntax

The JML syntax for expressions extends the Java syntax with several operators and primitives. See section 3.1 Extensions to Java Expressions for Predicates, for a brief description of the meaning of the JML syntax added to Java expressions.

The precedence of operators in JML expressions is similar to that in Java The precedence levels are given in the following table, where the parentheses, quantified expressions, [], ., and method calls on the first three lines all have the highest precedence, and for the rest, only the operators on the same line have the same precedence.

  highest   new () \forall \exists \max \min
                \num_of \product \sum informal-description 
                [] . and method calls 
            unary + and - ~ ! (typecast)
            * / % 
            + (binary) - (binary) 
            << >> >>> 
            < <= > >= <: instanceof 
            == != 
            & 
            ^ 
            | 
            && 
            || 
            ==> <== 
            <==> <=!=>
            ?:
  lowest    = *= /= %= += -= <<= >>= >>>= &= ^= |=

The following is the syntax of Java expressions, with JML additions. The additions are the operators ==>, <==, <==>, <=!=>, and <:, and the syntax found under the nonterminals jml-primary, set-comprehension, and spec-quantified-expr (see section B.1.10 Predicate and Specification Expression Syntax). The JML additions to the Java syntax can only be used in assertions and other annotations. Furthermore, within assertions, one cannot use any of the operators (such as ++, --, and the assignment operators) that would necessarily cause side effects.

expression-list ::= expression [ , expression ] ...
expression ::= assignment-expr 
assignment-expr ::= conditional-expr [ assignment-opt assignment-expr ]
assignment-op ::=  = | += | -= | *= | /= | %= | >>=  
        | >>>= | <<= | &= | `|=' | ^=
conditional-expr ::= equivalence-expr
                   [ ? conditional-expr : conditional-expr ]
equivalence-expr ::= implies-expr [ equivalence-op implies-expr ] ...
equivalence-op ::= <==> | <=!=>
implies-expr ::= logical-or-expr
             [ ==> implies-non-backward-expr ]
        | logical-or-expr <== logical-or-expr
             [ <== logical-or-expr ] ...
implies-non-backward-expr ::= logical-or-expr
             [ ==> implies-non-backward-expr ]
logical-or-expr ::= logical-and-expr [ `||' logical-and-expr ] ...
logical-and-expr ::= inclusive-or-expr [ && inclusive-or-expr ] ...
inclusive-or-expr ::= exclusive-or-expr [ `|' exclusive-or-expr ] ...
exclusive-or-expr ::= and-expr [ ^ and-expr ] ...
and-expr ::= equality-expr [ & equality-expr ] ...
equality-expr ::= relational-expr [ == relational-expr] ...
        | relational-expr [ != relational-expr] ...
relational-expr ::= shift-expr < shift-expr
        | shift-expr > shift-expr
        | shift-expr <= shift-expr
        | shift-expr >= shift-expr
        | shift-expr <: shift-expr
        | shift-expr [ instanceof type-spec ]
shift-expr ::= additive-expr [ shift-op additive-expr ] ...
shift-op ::= << | >> | >>>
additive-expr ::= mult-expr [ additive-op mult-expr ] ...
additive-op ::= + | -
mult-expr ::= unary-expr [ mult-op unary-expr ] ...
mult-op ::= * | / | %
unary-expr ::= ( type-spec ) unary-expr
        | ++ unary-expr
        | -- unary-expr
        | + unary-expr
        | - unary-expr
        | unary-expr-not-plus-minus
unary-expr-not-plus-minus ::= ~ unary-expr
        | ! unary-expr
        | ( builtinType ) unary-expr
        | ( reference-type ) unary-expr-not-plus-minus
        | postfix-expr
postfix-expr ::= primary-expr [ primary-suffix ] ... [ ++ ]
        | primary-expr [ primary-suffix ] ... [ -- ]
        | builtinType [ `[' `]' ] ... . class
primary-suffix ::= . ident
        | . this
        | . class
        | . new-expr
        | . super ( [ expression-list ] )
        | ( [ expression-list ] )
        | `[' expression `]'
        | [ `[' `]' ] ... . class
primary-expr ::= ident | new-expr 
        | constant | super | true
        | false | this | null
        | ( expression )
        | jml-primary
        | informal-description
builtInType ::= void | boolean | byte
        | char | short | int
        | long | float | double
constant ::= java-literal
new-expr ::= new type new-suffix
new-suffix ::= ( [ expression-list ] ) [ class-block ]
        | array-decl [ array-initializer ]
        | set-comprehension
array-decl ::= dim-exprs [ dims ]
dim-exprs ::= `[' expression `]' [ `[' expression `]' ] ...
dims ::= `[' `]' [ `[' `]' ] ...
array-initializer ::= { [ initializer [ , initializer ] ... [ , ] ] }
initializer ::= expression
        | array-initializer

B.2 Microsyntax or Lexical Grammar

Throughout the figures for the lexical grammar below, grammatical productions are to be understood lexically; that is, this grammar concerns individual characters, not tokens. Another way of thinking of this is that no white-space may intervene between the characters of a token.

The microsyntax of JML is described by the production microsyntax in the grammar 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

B.2.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 are special in that they cannot appear in some contexts where other whitespace can appear, and are also used to end C++-style (//) comments. This is described formally below.

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

B.2.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 ] ...

B.2.3 Comments

Both kinds of Java comments are allowed in JML: old C-style comments and new C++-style comments. However, if what looks like a comment starts with the at-sign (@) character, or with a plus sign and an at-sign (+@), then it is considered to be the start of an annotation by JML, 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-star [ non-star-slash ] ...
        | + non-at [ non-star-slash ] ...
        | stars-non-slash [non-star-slash] ...
non-star-slash ::= non-star
        | stars-non-slash
stars-non-slash ::= * [ * ] ... non-slash
non-at-plus-star ::= any character except @, +, or *
non-at ::= any character except @
non-star ::= any character except *
non-slash ::= any character except /
C-style-end ::= [ * ] ... */
C++-style-comment ::= // [ + ] end-of-line
        | // non-at-plus-newline [ non-newline ] ... newline
        | //+ non-at [ non-newline ] ... newline
non-newline ::= any character except a newline or carriage return
non-at-plus-newline ::= any character except @, +, newline, or carriage return

B.2.4 Annotation Markers

If what looks to Java like a comment starts with an at-sign (@) as its first character, then it is not considered a comment by JML. We refer to the tokens between //@ and the following newline, and between pairs of /*@ and @*/ as annotations.

Annotations must hold entire grammatical units of JML specifications. For example the following is illegal, because the postcondition 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.

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 (i.e., ignore) the character sequences that are annotation-markers: //@, //+@, /*@, /*+@, and @+*/, @*/. The at-sign (@) in @*/ is optional, and more than one at-sign may appear in the other annotation markers. However, JML will recognize jml-keywords only within annotations.

Within annotations, on each line, initial white-space followed by at-signs (@) are ignored. The definition of an annotation marker is given below.

annotation-marker ::= //@ | //+@
        | /*@ | /*+@ | @+*/ | @*/ | */
ignored-at-in-annotation ::= @

B.2.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 (i.e., not *) character on a line determines its interpretation. In particular, this means that the jml-pre and pre-jml tokens that start and end the jml-specs portion of a documentation comment are only recognized at the beginning of a line (following any leading * and whitespace).

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

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, is 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-newline [ non-end-of-line ] ...
    however, the start of the line must not match pre-jml or jml-pre
pre-jml ::= pre-tag [ doc-non-nl-ws ] ... jml-tag
jml-pre ::= end-jml-tag [ doc-non-nl-ws ] ... end-pre-tag
pre-tag ::= <pre> | <PRE>
end-pre-tag ::= </pre> | </PRE>
jml-tag ::= <jml> | <JML> | <esc> | <ESC>
end-jml-tag ::= </jml> | </JML> | </esc> | </ESC>

B.2.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-keywords represents the reserved words in Java (as in the JDK version 1.4). JML keywords are only recognized as such if they occur outside of a spec-expression but within either an annotation or a file that is a JML file (with suffixes `.jml' `.jml-refined', or `.refines-jml'). JML predicate keywords are, as their name implies, used within spec-expressions; they are also used in store-ref-lists and constrained-lists. The details are given below.

keyword ::= java-keyword | jml-predicate-keyword | jml-keyword
jml-predicate-keyword ::= \duration | \elemtype
        | \everything | \exists | \fields_of
        | \forall | \fresh | \invariant_for
        | \is_initialized | \lblneg | \lblpos
        | \lockset | \max | \min
        | \nonnullelements | \nothing | \not_modified
        | \not_specified | \num_of |\old
        | \other | \private_data | \product
        | \reach | \result | \space
        | \such_that | \sum | \type
        | \typeof | \TYPE  | \working_space 
jml-keyword ::= abrupt_behavior | accessible_redundantly | accessible
        | also | assert_redundantly
        | assignable_redundantly | assignable
        | assume_redundantly | assume | axiom
        | behavior | breaks_redundantly | breaks
        | callable_redundantly | callable | choose_if
        | choose | constraint_redundantly | constraint
        | continues_redundantly | continues
        | decreases_redundantly | decreases | decreasing_redundantly
        | decreasing | depends_redundantly | depends
        | diverges_redundantly | diverges  | duration_redundantly
        | duration | ensures_redundantly
        | ensures | example | exceptional_behavior
        | exceptional_example | exsures_redundantly | exsures
        | forall | for_example | ghost
        | implies_that | helper | hence_by_redundantly
        | hence_by | initializer | initially
        | instance | invariant_redundantly | invariant
        | loop_invariant_redundantly | loop_invariant
        | maintaining_redundantly | maintaining
        | measured_by_redundantly | measured_by
        | model_program | model | modifiable_redundantly
        | modifiable modifies_redundantly | modifies
        | monitored_by | monitored | non_null
        | normal_behavior | normal_example | nowarn
        | old | or | post | pre
        | pure | readable_if | refine
        | represents_redundantly | represents | requires_redundantly
        | requires | returns_redundantly | returns
        | set | signals_redundantly | signals
        | spec_protected | spec_public | static_initializer
        | subclassing_contract | uninitialized | unreachable
        | weakly | when_redundantly | when
        | working_space_redundantly | working_space

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 ::= decimal-numeral [ integer-type-suffix ]
decimal-numeral ::= 0 | non-zero-digit [ digits ]
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 | 0X hex-digit
        | hex-numeral 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-numeral hex-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. The exact syntax is given below.

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


Go to the first, previous, next, last section, table of contents.