7.1 Encoding of Expressions

The types expression_info, formula_info and assignable_info in attribute structures denote binary representation of BML expressions, formulas and assignable clauses respectively. They are represented as the prefix traversal sequence of the abstract syntax tree of a given expression, formula or assignable clause, with binary representation of operands.

The type formula_info is a subtype of expression_info, in the sense that all formulas are expressions, but not vice versa. To be a valid formula, the root of the abstract syntax tree must be one of 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;
     EQUIV = 0x08;
     NOTEQUIV = 0x09;
     FORALL_WITH_NAME = 0x0A;
     EXISTS_WITH_NAME = 0x0B;
     SINGLE_OCCURENCE = 0xBF;
     COND_EXPR = 0x64; // ?:

To be a valid expression, apart from the above constants, the root of the syntax tree can contain one of the following:

     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; // .
     THIS = 0x70;
     NULL = 0x72;
     FIELD_REF = 0x80;
     LOCAL_VARIABLE = 0x90;
     JAVA_TYPE = 0xC0;
     BOUND_VAR = 0xE0;
     EXPRESSION_ROOT = 0xBE;
     OLD = 0x99;
     TYPE_SMALL = 0x9A;
     NONNULLELEMENTS = 0x9B;

A root of a syntax tree representing an assignable clause (type assignable_info) must contain one of the following constants:

     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;
     MODIFIES_LIST = 0xDF;

[ JC 29/06/08 should be reviewed after code review of BMLlib]