5.2 JML Primary Expressions

BML basically supports the JML primary expressions that are part of JML level 0, except from the informal description (as explained in Relation with JML). This simplifies the syntax of jml-primary as follows.

     jml-primary ::= result-expression
             | old-expression
             | fresh-expression
             | nonnullelements-expression
             | typeof-expression
             | elemtype-expression
             | type-expression
             | spec-quantified-expr

Even though at bytecode level it is not necessary to precede every keyword with the \-symbol to avoid name clashes with program variables, for compatibality, also in BML all specification-specific expressions start with a \-symbol. Moreover, this will avoid name clashes when the specification is displayed with original variable names; although this might not cause problems for the tools, it might be confusing for the user.

The grammar for quantified expressions is the same as in JML. Notice that BML supports all quantified expressions, also those that are not part of JML level 0. The bound variables that are declared in the expressions are stored in the second constant pool, where all specification-only constructs are stored, and internally represented as indexes into this second pool. However, a tool will typically display the specification using the bound variable name.

The semantics of these JML primary expressions, used in a BML specification, coincides with the semantics described in Section 11.4 of JML Reference Manual.