Previous: Bibliography, Up: Top
The following is a summary of the context-free grammar for BML.
init-declarator-list ::= init-declarator [ , init-declarator ] ...
classfile ::= fileheader typeheader typebody
fileheader ::= packageinfo constant-pools
packageinfo ::= package packagename nl [ nl ]...
packagename ::= [default] | typename
constant-pools ::= constant-pool [ second-constant-pool ] nl
constant-pool ::= Constant pool: nl constant-pool-content
second-constant-pool ::= Second constant pool: nl constant-pool-content
constant-pool-content ::= constant-pool-line nl [ constant-pool-line nl ]...
constant-pool-line ::= const cp-ref = constant-pool-entry [ constant-pool-comment ]
constant-pool-entry ::= class-cp-entry | field-cp-entry
| method-cp-entry | interface-method-cp-entry
| string-cp-entry | integer-cp-entry | float-cp-entry
| long-cp-entry | double-cp-entry
| name-and-type-cp-entry | utf8-cp-entry
class-cp-entry ::= Class cp-ref;
field-cp-entry ::= Fieldref cp-ref.cp-ref;
method-cp-entry ::= Methodref cp-ref.cp-ref;
interface-method-cp-entry ::= InterfaceMethodref cp-ref.cp-ref;
string-cp-entry ::= String cp-ref;
integer-cp-entry ::= Integer [ sign ] decimal-integer-literal;
float-cp-entry ::= Float [ sign ] floating-point-literal;
long-cp-entry ::= Long [ sign ] decimal-integer-literal;
double-cp-entry ::= Double [ sign ] floating-point-literal;
name-and-type-cp-entry ::= NameAndType cp-ref.cp-ref;
utf8-cp-entry ::= Utf8 [ string-character ]...;
cp-ref ::= #decimal-numeral
constant-pool-comment ::= // [ non-end-of-line ]...
typename ::= ident[/typename]
typeheader ::= classmodifiers class ident
[ class-extends-clause ] [ implements-clause ] nl...
| interfacemodifiers interface ident
[ interface-extends-clause ] [ implements-clause ] nl...
classmodifiers ::= [ classmodifier ]...
interfacemodifiers ::= [ interfacemodifier ]...
classmodifier ::= public | protected | private
| abstract | static
| final | strictfp
interfacemodifier ::= public | protected | private
| abstract | static |
| strictfp
class-extends-clause ::= extends typename
interface-extends-clause ::= extends name-list
implements-clause ::= implements name-list
name-list ::= typename [, typename ]...
typebody ::= [ staticsection ] [ objectsection ] [ methods ]
staticsection ::= [ staticfields ] [ staticspec ]
staticspec ::= [ staticinvariants ] [ staticconstraints ]
[ staticrepresents ] [ staticinitially ]
objectsection ::= [ objectfields ] [ objectspec ]
objectspec ::= [ objectinvariants ] [ objectconstraints ]
[ objectrepresents ] [ objectinitially ]
staticfields ::= [ staticfield ]...
objectfields ::= [ objectfield ]...
staticinvariants ::= [ static invariant nl ]...
staticconstraints ::= [ static history-constraint nl ]...
staticrepresents ::= [ static represents-decl nl ]...
staticinitially ::= [ static initially-clause nl ]...
objectinvariants ::= [ invariant nl ]...
objectconstraints ::= [ history-constraint nl ]...
objectrepresents ::= [ represents-decl nl ]...
objectinitially ::= [ initially-clause nl ]...
methods ::= [ method ]...
staticfield ::= static field
objectfield ::= field
classfile ::= fileheader typeheader typebody
fileheader ::= packageinfo constant-pools
packageinfo ::= package packagename nl [ nl ]...
packagename ::= [default] | typename
constant-pools ::= constant-pool [ second-constant-pool ] nl
constant-pool ::= Constant pool: nl constant-pool-content
second-constant-pool ::= Second constant pool: nl constant-pool-content
constant-pool-content ::= constant-pool-line nl [ constant-pool-line nl ]...
constant-pool-line ::= const cp-ref = constant-pool-entry [ constant-pool-comment ]
constant-pool-entry ::= class-cp-entry | field-cp-entry
| method-cp-entry | interface-method-cp-entry
| string-cp-entry | integer-cp-entry | float-cp-entry
| long-cp-entry | double-cp-entry
| name-and-type-cp-entry | utf8-cp-entry
class-cp-entry ::= Class cp-ref;
field-cp-entry ::= Fieldref cp-ref.cp-ref;
method-cp-entry ::= Methodref cp-ref.cp-ref;
interface-method-cp-entry ::= InterfaceMethodref cp-ref.cp-ref;
string-cp-entry ::= String cp-ref;
integer-cp-entry ::= Integer [ sign ] decimal-integer-literal;
float-cp-entry ::= Float [ sign ] floating-point-literal;
long-cp-entry ::= Long [ sign ] decimal-integer-literal;
double-cp-entry ::= Double [ sign ] floating-point-literal;
name-and-type-cp-entry ::= NameAndType cp-ref.cp-ref;
utf8-cp-entry ::= Utf8 [ string-character ]...;
cp-ref ::= #decimal-numeral
constant-pool-comment ::= // [ non-end-of-line ]...
typename ::= ident[/typename]
typeheader ::= classmodifiers class ident
[ class-extends-clause ] [ implements-clause ]
| interfacemodifiers interface ident
[ interface-extends-clause ] [ implements-clause ]
classmodifiers ::= [ classmodifier ]...
interfacemodifiers ::= [ interfacemodifier ]...
classmodifier ::= public | protected | private
| abstract | static
| final | strictfp
interfacemodifier ::= public | protected | private
| abstract | static |
| strictfp
class-extends-clause ::= extends typename
interface-extends-clause ::= extends name-list
implements-clause ::= implements name-list
name-list ::= typename [, typename ]...
typebody ::= [ staticsection ] [ objectsection ] [ methods ]
staticsection ::= [ staticfields ] [ staticspec ]
staticspec ::= [ staticinvariants ] [ staticconstraint ]
[ staticrepresents ] [ staticinitially ]
objectsection ::= [ objectfields ] [ objectspec ]
objectspec ::= [ objectinvariants ] [ objectconstraint ]
[ objectrepresents ] [ objectinitially ]
staticfields ::= [ staticfield ]...
objectfields ::= [ objectfield ]...
methods ::= [ method ]...
modifiers ::= [ modifier ] ...
modifier ::= public | protected | private
| abstract | static |
| final | synchronized
| transient | volatile
| native | strictfp
| const
bml-modifier ::= spec_public | spec_protected
| model | ghost | pure
| helper | non_null | nullable
| peer | rep | readonly
field ::= [ nsfieldmodifiers ] type ident ;
clinit ::= [ methodspec ] clinitheader [ methodbody ]
method ::= [ methodspec ] methodheader [ methodbody ]
type ::= typename | field-built-in-type
field-built-in-type ::= boolean | byte
| char | short | int
| long | float | double
nsfieldmodifiers ::= public | protected | private
| final | strictfp
| spec_public | spec_protected | model
| ghost
| non_null | nullable
| peer | rep | readonly
bml-declaration ::= invariant
| history-constraint
| represents-decl
| initially-clause
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 | field-built-in-type
constant ::= java-literal
type-spec ::= arr-type
| \TYPE [ dims ]
arr-type ::= [ ownership-modifiers ] 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 )