Repair/RepairCompiler/cdl.tex

   1 Constraint Definition Language
   2 xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
   3
   4 constraints ::= constraints constraint | constraint
   5
   6 constraint ::= optcrash OPENBRACKET quantifiers CLOSEBRACKET COMMA body SEMICOLON
   7
   8 optcrash ::= CRASH | /* nothing */
   9
  10 quantifiers ::= quantifiers COMMA quantifier | quantifier | /* nothing */
  11
  12 quantifier ::= FORALL ID:var IN set:set
  13
  14 set ::= ID:setname
  15       | OPENBRACE listofliterals CLOSEBRACE
  16
  17 listofliterals ::= listofliterals COMMA literal | literal
  18
  19 body ::= body AND body
  20        | body OR body
  21        | NOT body
  22        | OPENPAREN body CLOSEPAREN
  23        | predicate
  24
  25 predicate ::= SIZEOF OPENPAREN setexpr CLOSEPAREN limitedcompare DECIMAL:dec
  26             | ID:var IN setexpr
  27             | ID:var DOT ID:relation compare:compare expr
  28
  29 setexpr ::= ID:var
  30           | ID:var DOT ID:relation
  31           | ID:var DOTINV ID:relation
  32
  33 expr ::= ID:var
  34        | OPENPAREN expr CLOSEPAREN
  35        | LITERAL OPENPAREN literal CLOSEPAREN
  36        | expr operator expr
  37        | expr DOT ID:field
  38        | SIZEOF OPENPAREN setexpr CLOSEPAREN
  39        | CAST OPENPAREN ID:type COMMA expr CLOSEPAREN
  40
  41 operator ::= ADD | SUB | MULT | DIV
  42
  43 literal ::= TRUE | DECIMAL | STRING | CHAR | ID
  44
  45 limitedcompare ::= EQUALS | wGT
  46
  47 compare ::= LT | GT | LE | GE | EQUALS
  48
  49
  50