converting grammar (written in ANTLR) of a language into formal language/mathematical notations

Question

In my current project, my boss has assigned a job of expressing a grammar (written in ANTLR) of domain specific language into formal language/notations. For instance, the following is a small code snippet of grammar.

     vocabSpec : 'resources' ':' resources_def ;   // Resource definition 

     resources_def :
          'sensors' ':'   (sensor_def)+   // Sensor definition
          'actuators' ':' (actuator_def)+  // Actuator definition       
         ;

     sensor_def:
        CAPITALIZED_ID  
        (sensorMeasurement_def ';')* ;

      sensorMeasurement_def : 'generate' lc_id ':'  CAPITALIZED_ID ;

    // Actuator definition : Actuator name, actions and its parameters 

      actuator_def: CAPITALIZED_ID  (action_def ';')* ;

      action_def: 'action' CAPITALIZED_ID '(' (parameter_def)? ')'  ;

      parameter_def :  lc_id ':'  CAPITALIZED_ID (',' parameter_def )?  ;

      lc_id: ID ;

      ID  : 'a'..'z'  ('a'..'z' | 'A'..'Z' )* ;

      CAPITALIZED_ID: 'A'..'Z' ('a'..'z' | 'A'..'Z' )*;

As per my knowledge, ANTLR grammar of any language is itself a formal specification. I have no idea -- How can I specify this grammar is formal way. Could you please give me pointers for writing the above grammar into formal specification/mathematical notations ?

Answer 1

Yes, an ANTLR grammar is a formal system. Based on this, you can just declare victory with a straight face.

He probably wants something other than ANTLR syntax. And, rightfully so, the annotations in the ANTLR grammar for building trees, etc, just confuse the issue, as do the various lookaheads. So, in your shoes, I'd remove all the annotations, and probably recast the grammar into IEEE EBNF (See http://en.wikipedia.org/wiki/Extended_Backus%E2%80%93Naur_Form). And you can point him to that web page, and declare you have a "pure context free grammar".