|
|
|---|
|
|
|
|---|
A fornalization of the ABNF notation.
We formalize the syntax and semantics of the ABNF notation.
We start with an abstract syntax of ABNF, derived from the concrete syntax. Even though the concrete syntax is specified in ABNF, we do not use ABNF to specify this abstract syntax, thus avoiding the meta-circularity.
Then we define a semantics of ABNF based on the abstract syntax, in terms of matching relations between (concrete syntax) trees and abstract syntactic entities.
With a formal semantics in hand, we proceed to formalize the concrete syntax of ABNF using ABNF itself, as follows.
The files
Since at this point of the bottom-up development of the formalization we do not yet have a formalization of the concrete syntax of ABNF, we cannot directly use the contents of those two files to formalize the concrete syntax of ABNF, again for meta-circular reasons. We break that circularity by writing those rules in abstract syntax, deriving them from the contents of the files.
To make the rules written in abstract syntax look more like if they were written in concrete syntax, we introduce some convenience constructors for ABNF abstract syntax. We use them to define, in abstract syntax, the core rules and the concrete syntax rules. We perform some validation of the core rules and some validation of the concrete syntax rules, using some of the grammar operations.
We put concrete syntax rules and (the used) core rules together to formalize the concrete syntax, making use of the ABNF semantics applied to the grammar of ABNF (in its abstract syntax form, which is what the semantics is defined on).
To complete the formalization of the ABNF notation, we formalize the relation between concrete and abstract syntax via a syntax abstraction mapping from concrete syntax trees of ABNF to abstract syntax tree of ABNF.
We also perform some validation of the concrete syntax, via some of the grammar operations.
With a formalization of the ABNF notation in hand, we develop a verified parser of ABNF grammars, whose verification rests on the formalization of the ABNF notation. The parser is not part of the formalization of the ABNF notation, but we use it to validate the meta-circularity with which [RFC] defines the syntax of ABNF.