Appendix A Grammar Summary

The following is a summary of the context-free grammar for BML.

A.1 Notations and Conventions Used

     
init-declarator-list ::= init-declarator [ , init-declarator ] ...
classfile ::= fileheader classheader classbody
fileheader ::= packageinfo [imports]
classheader ::= Java class header
classbody ::= [ staticsection ] [ objectsection ] constructors [ methods ]
staticsection ::= [ staticfields ] [ staticspec ]
staticspec ::= [ staticinvariant ] [ staticconstraint ]
                        [ staticrepresents ] [ staticinitially ]
objectsection ::= [ objectfields ] [ objectspec ]
objectspec ::= [ objectinvariant ] [ objectconstraint ]
                          [ objectrepresents ] [ objectrepresents ]
constructors ::= constructor [ constructor ]...
imports ::= [ import ]...
staticfields ::= [ staticfield ]...
objectfields ::= [ objectfield ]...
methods ::= [ method ]...
method ::= [ methodspec ] methodheader [ methodbody ]

A.2 Class and Interface Specifications

     
modifiers ::= [ modifier ] ...
modifier ::= public | protected | private
             | abstract | static |
             | final | synchronized
             | transient | volatile
             | native | strictfp
             | const
bml-modifier ::= spec_public | spec_protected
             | model | ghost | pure
             | static | helper
             | non_null | nullable
             | ownership-modifier
ownership-modifier ::= peer | rep | readonly
bml-declaration ::= invariant
             | history-constraint
             | represents-decl
             | initially-clause

A.3 Predicates and Specification Expressions

     
expression-list ::= expression [ , expression ] ...
expression ::= conditional-expr
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-not-plus-minus
unary-expr-not-plus-minus ::= ~ unary-expr
             | ! unary-expr
             | ( built-in-type ) unary-expr
             | ( reference-type ) unary-expr-not-plus-minus
             | postfix-expr
postfix-expr ::= primary-expr [ primary-suffix ] ...
             | built-in-type [ `[' `]' ] ... . class
primary-suffix ::= . #nat
             | . super ( [ expression-list ] )
             | . ident ( [ expression-list ] )
             | `[' expression `]'
             | [ `[' `]' ] ... . class
primary-expr ::= lv[nat] |
             | ident | constant | super | true
             | false | this | null
             | ( expression )
             | jml-primary
             | bml-primary
built-in-type ::= void | boolean | byte
             | char | short | int
             | long | float | double
constant ::= java-literal
type-spec ::= [ ownership-modifier ] type [ dims ]
              | \TYPE [ dims ]
type ::= reference-type | built-in-type
reference-type ::= name
dims ::= `[' `]' [ `[' `]' ] ...
jml-primary ::= result-expression
             | old-expression
             | fresh-expression
             | nonnullelements-expression
             | typeof-expression
             | elemtype-expression
             | type-expression
             | spec-quantified-expr
bml-primary ::= cntr-expression
             | stack-expression
             | arraylength-expression
cntr-expression ::= \cntr
stack-expression ::= \st( additive-expr )
arraylength-expression ::= \length( expression )