anchor.diff:    | 'while' '(' exp ')' NL* t='{'
       ( NL* 'l"""' loopInvariant '"""' )?
       blockEnd                                            #WhileStmt
  -  | ID 'match' '{' matchCase+ '}'                       #MatchStmt
  +  | exp 'match' '{' matchCase+ '}'                      #MatchStmt
     | op=( 'print' | 'println' )
       '(' ( stringOrExp ( ',' stringOrExp )* )? ')'       #PrintStmt
     | tb=ID '(' index=exp ')' '=' NL? r=exp               #SeqAssignStmt
     | methodDecl                                          #MethodDeclStmt
     | traitDecl                                           #TraitDeclStmt
     | recordDecl                                          #RecordDeclStmt
  +  | enumDecl                                            #EnumDeclStmt
  +  | objectDecl                                          #ObjectDeclStmt
     | 'l"""'
       ( proof
       | sequent
       | invariants
  -    | facts
  +    | proofElements
       ) '"""'                                             #LogikaStmt
     | impor                                               #ImportStmt
     | exp                                                 #ExpStmt
  
positive.code:     // org=="org" && sireum=="sireum" && logika=="logika"
    ;
  
  facts
    : '{' NL*
      ftb='fact' NL*
      factOrFun ( NL+ factOrFun? )*
      te='}' NL* ;
  
  factOrFun: fact | fun ;
  
  fact: ID '.' formula ;
  
  fun
    : tb='def' ID  NL?
      '(' param ( ',' param )* ')' ':' type
      funDef?
    ;
  
negative.code: 
  loopInvariant
    : tb='{' NL*
      reads?
      modifies
      te='}' NL*
    | tb='{' NL*
      itb='invariant' NL* formula ( NL+ formula? )*
      reads?
      modifies?
      te='}' NL*
    ;
  
  modifies
    : tb='modifies' name ( ',' name )* NL* ;
  
  methodContract
    : tb='{' NL*
      contract NL*
      ( subContract ( NL+ subContract )*  NL* )?
      te='}' NL*
    ;
  
  contract
    : reads?
      ( ( 'requires' | 'pre' ) NL*
        rs+=formula ( NL+ rs+=formula? )* )? NL*
      modifies?
      ( ( 'ensures' | 'post' ) NL*
        es+=formula ( NL+ es+=formula? )* )?
    ;
  
  subContract
    : ID '.' contract
    ;
  
  reads
    : tb='reads' name ( ',' name )* NL* ;
  
  invariants
    : tb='{' NL*
  