Previous: BML Operators, Up: Predicates and Specification Expressions


5.5 Store Refs

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.