HoareRulesのラベル

nmTokenをああいう定義にすると、name⊂nmToken、integer⊂nmTokenになってしまって、どうも気持ち悪いですね。

しかし、たいていのレクサー・ジェネレータは文脈により字句解析規則を切り替えることができるだろうから、ラベルの認識は別な文脈にすることにしましょう。つまり：

/* ルール全体のトップレベルでのみ認識される字句 */

labelChar ::= [-._a-zA-Z0-9] // ハイフンとピリオドも許すことにした

labelToken ::= labelChar+
/* ルール全体の構文定義 */

rule ::= '[' labelToken ']' preCondition action postCondition ';'

labelTokenの定義はルール・トップレベルの、'['から']'のあいだだけで有効。nameやnumberは別な文脈で認識されるので、かぶることはなくなります。