Home » forums » LtU Forum

Correctness of Parsers

Hi all,

I'm looking for literature which focuses on proving context-free parsers correct. For example, I have work by Sikkel on Parsing Schemata and work by Cliff Jones on formalizing Earley's algorithm, and looking for other ways that people have formalized and proved those (and other context-free) parsers.

Thanks for any recommendations,
Dan

By Daniel Zingaro at 2007-06-01 03:59 | LtU Forum | previous forum topic | next forum topic | other blogs | 4918 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Correctness of parsers

If you construct a parser using declarative programming techniques and parser combinators, then your program is not just a parser but a precise specification of what is to be parsed. Thus, it's correct by design.

Of course, your specification might be erroneous, in which case you've produced a correct parser for the wrong specification.

Determining whether your parser specification matches some external specification, such as the combination of English prose and BNF grammar in the ISO C++ language specification, then requires one to manually compare both and convince onesself that the specification is what it should be.

This highlights the ultimate limitation of the "proofs as programs". You can produce a machine-verifyable proof that your program meets its specification, but can you be sure that you specified the right thing?

By Tim Sweeney at Mon, 2007-06-04 18:35 | login or register to post comments