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 Combined 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.