Next: Typechecking BML, Previous: Annotation (of) Statements, Up: Top
The encoding of BML specifications in class files is done via
attributes: class attributes, field attributes, method attributes and
code attributes. They use a binary representations of expressions
(type expression_info), formulas (type formula_info) and
assignable clauses (type assignable_info), written as a prefix
encoding of the abstract syntax tree of the expression, with the
following constants:
TRUE = 0x00;
FALSE = 0x01;
AND = 0x02;
OR = 0x03;
IMPLIES = 0x04;
NOT = 0x05;
FORALL = 0x06;
EXISTS = 0x07;
EQ = 0x10;
GRT = 0x11;
LESS = 0x12;
LESSEQ = 0x13;
GRTEQ = 0x14;
NOTEQ = 0x17;
PLUS = 0x20;
MINUS = 0x21;
MULT = 0x22;
DIV = 0x23;
REM = 0x24;
NEG = 0x25;
BITWISEAND = 0x30;
BITWISEOR = 0x31;
BITWISEXOR = 0x32;
SHL = 0x33;
USHR = 0x34;
SHR = 0x35;
INT_LITERAL = 0x40;
RESULT = 0x52;
ARRAYLENGTH = 0x56;
ARRAY_ACCESS = 0x61;
FIELD_ACCESS = 0x63; // .
COND_EXPR = 0x64; // ?:
THIS = 0x70;
OLD_THIS = 0x71;
NULL = 0x72;
FIELD_REF = 0x80;
OLD_FIELD_REF = 0x81;
LOCAL_VARIABLE = 0x90;
OLD_LOCAL_VARIABLE = 0x91;
JAVA_TYPE = 0xC0;
MODIFIES_EVERYTHING = 0xD0;
MODIFIES_NOTHING = 0xD1;
MODIFIES_IDENT = 0xD2;
MODIFIES_DOT = 0xD3;
MODIFIES_ARRAY = 0xD4;
MODIFIES_INTERVAL = 0xD5;
MODIFIES_SINGLE_INDEX = 0xD6;
MODIFIES_STAR = 0xD7;
BOUND_VAR = 0xE0;
EQUIV = 0x08;
NOTEQUIV = 0x09;
FORALL_WITH_NAME = 0x0A;
EXISTS_WITH_NAME = 0x0B;
SINGLE_OCCURENCE = 0xBF;
EXPRESSION_ROOT = 0xBE;
MODIFIES_LIST = 0xDF;
OLD = 0x99;
The constants referenced in BML-related attributes that are not defined in the constant pool (see Constant Pool) are stored in the second constant pool (see Class Attributes) which is one of the class attributes (see Class Attributes). The constants are referenced by numbers: if the number n is small enough it is an index in the first constant pool and if it is larger than the size of the first constant pool (cp_count) then it is a reference to the constant number (n - cp_count) in the second constant pool.