|
|
|---|
|
|
|
|---|
A verified executable parser of ABNF grammars.
It may be possible to derive this parser from parse-grammar* (or a variant of it that resolves the ambiguity discussed there) via transformational refinements, but here we write an implementation directly and we prove its correctness.
The implementation and verification techniques employed for this parser seem more general than the parser. They should be applicable to parsers of other languages specified in ABNF, e.g. to HTTP parsers. It may also be possible to build a parser generator that turns ABNF grammars (satisfying certain restrictions, as with typical parser generators) into verified executable parsers, i.e. executable parsers accompanied by proofs of correctness.