5.1 BML Expressions that are Directly Inherited from JML

The BML syntax for expressions is a simplification of the JML expression syntax, with a few extra primary expressions, specific to properties that one would like to express about bytecode.

The precedence of operators in BML 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 two lines all have the highest precedence, while ?: has the lowest.

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

The following is the syntax of BML 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

For completeness, we repeat the grammar of type-spec from Section 7.1.2.2 of the JML Reference Manual, because this shows how the ownership modifiers can be declared (see Class Member Declarations for a discussion of ownership types in BML).

     type-spec ::= [ ownership-modifier ] type [ dims ]
              | \TYPE [ dims ]
     type ::= reference-type | built-in-type
     reference-type ::= name
     dims ::= `[' `]' [ `[' `]' ] ...

An important difference with the JML grammar is that BML expressions do not contain variable identifiers. Instead, we have references into the constant pool (written #n) and to the local variable table (written lv[n]) (where n is some natural number in the range of the (second) constant pool/local variable table, respectively). However, if the original source code exists, and is available, typically BML tools will provide the possibility to see the specification expressions with the original source code level identifiers, even though the internal representation uses the bytecode level references.

In BML, all field accesses and method calls have to be qualified, i.e., the receiver object has to be explicitly mentioned. Notice that this is similar to the treatment of field accesses and method invocations in bytecode, where the receiver object is always explicit. Therefore, references to the constant pool can only occur in primary-suffix expressions. Similarly, method calls, i.e., the case .ident(expression-list), where ident is a method name can only occur in primary-suffix. However, to allow calls to static methods, the grammar allows identifiers as primary-expr. Type checking will enforce that these are class names. In contrast, accesses to local variables are always unqualified, thus an expression lv[n] has to be a primary-expr expression.

The semantics of these expressions is the same as for JML, as discussed in Section 11.3 of the JML Reference Manual.