5.3 BML Primary Expressions

BML also defines several primary expressions that are specific to bytecode (and do not have any JML/Java source code counterpart). BML primary expressions have the following grammar.

     bml-primary ::= cntr-expression
             | stack-expression
             | arraylength-expression

5.3.1 Counter of the Operand Stack

The syntax of a cntr-expression is as follows:

     cntr-expression ::= \cntr

The primary \cntr can only be used in annotation statements (that is: assert, assume, set, and unreachable statements, and loop specifications, see Annotation (of) Statements). Its value is the current size of the operand stack.

5.3.2 Stack Expressions

The syntax of a stack-expression is as follows:

     stack-expression ::= \st( additive-expr )

A stack-expression can only be used in annotation statements (that is: assert, assume, set, unreachable and debug statements, and loop specifications, see Annotation (of) Statements).

An expression of the form \st(N) refers to the value of the Nth element on the operand stack. The value of the argument expression N should be between 0 and the value of \cntr, i.e., in the range of the operand stack. A typical use of a stack expression is to specify a property on the value of the top element of the operand stack.

For example, the top of the operand stack is greater than 3, or it is greater than the next value on the stack:

     // assert \st(\cntr - 1) > 3 || \st(\cntr - 1) > \st(\cntr - 2);

5.3.3 Arraylength

The syntax of an arraylength-expression is as follows:

     arraylength-expression ::= \length( expression )

An arraylength-expression can be used without restrictions. If Expr is an expression with as type a reference to an array, the expression \length(Expr) denotes the length of the array pointed to be Expr. If Expr does not point to an array this is a typing error. At source code level, for every array a, the expression a.length can be used to inspect the length of the array. Occurrence of such an expression in the program code compiles into the special bytecode instruction arraylength. The BML arraylength-expression allows to express properties using the array length also in bytecode-level specifications. Thus, given that the source code level expression (with array type) Expr-s compiles into the bytecode level expression Expr-b, the semantics of \length(Expr-b) corresponds to the semantics of Expr-s.length.