Next: BML operators, Previous: JML Primary Expressions, Up: Predicates and Specification Expressions
[INRIA: BUT, do we want \ for bml-primary, or not?]
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