Previous: BML Operators, Up: Predicates and Specification Expressions
BML also supports the same store refs expressions as JML, except that
variable names ident internally are replaced by references into
the constant pool (#nat) or to the local variable table
(lv[nat]). Their semantics is as described in
Section 11.7 of the JML Reference Manual.