Next: JML Primary Expressions, Previous: Predicates and Specification Expressions, Up: Predicates and Specification Expressions

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-exprconditional-expr::=equivalence-expr[`?`

conditional-expr`:`

conditional-expr]equivalence-expr::=implies-expr[equivalence-opimplies-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-opadditive-expr] ...shift-op::=`<<`

|`>>`

|`>>>`

additive-expr::=mult-expr[additive-opmult-expr] ...additive-op::=`+`

|`-`

mult-expr::=unary-expr[mult-opunary-expr] ...mult-op::=`*`

|`/`

|`%`

unary-expr::=`(`

type-spec`)`

unary-expr|`+`

unary-expr|`-`

unary-expr|unary-expr-not-plus-minusunary-expr-not-plus-minus::=`~`

unary-expr|`!`

unary-expr|`(`

built-in-type`)`

unary-expr|`(`

reference-type`)`

unary-expr-not-plus-minus|postfix-exprpostfix-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-primarybuilt-in-type::=`void`

|field-built-in-typeconstant::=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::=arr-type|`\TYPE`

[dims]arr-type::= [ownership-modifiers]type[dims]type::=reference-type|built-in-typereference-type::=namedims::= ``[`

' ``]`

' [ ``[`

' ``]`

' ] ...

Notice that the BML grammar allows one to use identifiers in
expressions, even though internally these are always represented by
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 Combined 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. Similarly, if a user edits a BML
specification directly, he or she is allowed to use identifiers in the
specifications.

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.