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).
- An abstractor from ABNF concrete syntax to ABNF abstract syntax.
- Executable operations on ABNF grammars,
e.g. to check their well-formedness and to compose them.
- Examples of use of the parser, the abstractor, and some grammar operations
on a few real-world ABNF grammars (e.g. for HTTP).
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 formalization of the ABNF notation
and of the verified parser
(but not of the operations on ABNF grammars).
The differences between the paper and the ABNF library
are described here.
Subtopics
- Parser-generators
- Tools to generate parsing functions.
- Concrete-to-abstract-syntax
- An executable mapping from
the concrete syntax of ABNF to the abstract syntax of ABNF.
- Semantics
- Semantics of ABNF.
- Abstract-syntax
- Abstract syntax of ABNF.
- Grammar-parser
- A verified executable parser of ABNF grammars.
- Parsing-primitives-seq
- Some basic ABNF parsing functions for use with Seq.
- Parsing-primitives-defresult
- Some basic ABNF parsing functions
for use with fty::defresult.
- Core-rules
- Core rules of ABNF.
- Differences-with-paper
- Differences with the paper.
- Examples
- Some real-world examples of ABNF grammars.
- Parser-and-abstractor-validation
- A validation of the parser and abstractor.
- Operations
- Operations on ABNF grammars.
- Concrete-syntax
- Concrete syntax of ABNF.
