|
|
|---|
|
|
|
|---|
A validation of the meta-circularity in the concrete syntax definition of ABNF.
[RFC] defines the concrete syntax of ABNF meta-circularly, using ABNF. Our formalization of the concrete syntax of ABNF is not meta-circular, because it would be impossible in a theorem prover like ACL2. Nonetheless, here we provide a validation of the meta-circularity.
We use the verified grammar parser and the executable syntax abstractor to parse and abstract the core rules and the concrete syntax rules, from the respective grammar files, and we show that we obtain exactly the same rules, in abstract syntax, that we manually define for the core rules and for the concrete syntax rules. In other words, the same grammar rules that we write manually are obtained by correctly processing the grammar files (where `correctly' refers to the fact that the grammar parser is verified).