Next: Loop Statements, Previous: Annotation Statements, Up: Annotation (of) Statements
As JML, BML allows one to declare local ghost variables. Their semantics is as described in Section 12.1 of the JML Reference Manual.
Each method info attribute is extended with a local ghost variable attribute, that contains the local ghost variables declared in that method. The format of the local ghost variable attribute is similar to that of the local variable table, i.e., for each local ghost variable it is defined in which range it is valid.