このドキュメントでは、¬<><∪∪の文法を Input Specification よりも厳密に定義します。ゴール記号は Root です。この文法は、¬<><∪∪のソースファイルで使用されているものを基にしているため、終端・非終端記号の名前は Input Specification などで使用されているものとは異なります。? は省略可能、* は0回以上の繰り返しを表します。
StringLiteral ::= <Javaの文字列リテラル> CharacterLiteral ::= <Javaの文字リテラル> IDENTIFIER ::= <Javaの識別子および予約語で、$で始まらないもの>
加えて、以下においてJavaの文字列リテラルの形式で表現される文字列も終端記号となります。また、次の文字列も終端記号となります。"||" "&&" "--" "!!" "**" "++" "??"