Abnf
A library for ABNF (Augmented Backus-Naur Form).
ABNF is a standardized formal grammar notation
used in several Internet syntax specifications,
e.g. URI, HTTP, IMF, SMTP, IMAP, and JSON. ABNF is specified by RFC 5234 and RFC 7405; the latter updates two portions of the former.
The syntax of ABNF is specified in ABNF itself.
This ACL2 library provides:
- A formalization of the syntax and semantics of the ABNF notation.
- A verified parser that turns ABNF grammar text
(e.g. from the HTTP RFC)
into a formal representation suitable for formal specification
(e.g. for HTTP parsing).
- Executable operations on ABNF grammars,
e.g. to check their well-formedness and to compose them.
- A defgrammar tool
for building ACL2 representations of grammar from files,
using the aforementioned verified parser,
and for automatically proving
certain properties such as well-formedness.
- Some basic parsing primitives, also available in another variant, usable as part of larger parsers.
- A defdefparse tool
for generating some very preliminary tools to generate
parsing functions from grammar rules.
- Some examples of
use of defgrammar and some grammar operations
on a few real-world ABNF grammars (e.g. for HTTP).
Besides the aforementioned examples,
defgrammar and some grammar operations have been used on an ABNF grammar of Java, two ABNF grammars of Yul, and an ABNF grammar of a subset of C. The defdefparse tool has been used to generate part of a Yul lexer.
In the documentation of this library,
`[RFC]' refers to the result of updating RFC 5234 as specified by RFC 7405.
Sections and subsections of [RFC] are referenced
by appending their designations separated by colon:
for example, `[RFC:3]' refers to Section 3 of RFC 5234.
As another example, `[RFC:2.3]' refers to
the result of updating Section 2.3 of RFC 5234
as specified in Section 2.1 of RFC 7405.
These square-bracketed references may be used
as nouns or parenthetically.
This VSTTE 2018 paper provides an overview
of the ABNF notation formalization
and of the verified parser
(but not of the operations on ABNF grammars,
of the parsing primitives,
of the parsing generation tools,
or of the real-world examples).
The differences between the paper and the ABNF library
are described here.
Subtopics
- Deftreeops
- Generate grammar-specific operations on trees.
- Defdefparse
- Generator of tools to generate parsing functions.
- Defgrammar
- Build an ACL2 representation of an ABNF grammar from a file.
- Tree-utilities
- Some utilities to manipulate ABNF trees.
- Notation
- A fornalization of the ABNF notation.
- Grammar-parser
- A verified executable parser of ABNF grammars.
- Meta-circular-validation
- A validation of the meta-circularity in
the concrete syntax definition of ABNF.
- Parsing-primitives-defresult
- Some basic ABNF parsing functions
for use with fty::defresult.
- Parsing-primitives-seq
- Some basic ABNF parsing functions for use with Seq.
- Operations
- Operations on ABNF grammars.
- Examples
- Some real-world examples of ABNF grammars.
- Differences-with-paper
- Differences with the paper.
- Constructor-utilities
- Some utilities to construct ABNF abstract syntax.
- Grammar-printer
- A pretty-printer of ABNF grammars.
- Parsing-tools
- Some tools to build parsers for ABNF-defined languages.
