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:
Besides the aforementioned examples, the parser, abstractor, and some grammar operations have been used on an ABNF grammar of Java, an ABNF grammar of Yul, and an ABNF grammar of a subset of C. The parsing generation tools have 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, of the verified parser, and of the syntax abstractor (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.