I am wondering about how to give a correctness prove of a simple
parsing
algorithm. I tried to think of a simple example but even in this
case I
don't know how.
I'm not sure I understand your question, but I'm guessing you're
looking for general techniques for the formal verification of
combinator-based parsers. Here's a quick brain dump of related work
that might help you get started.
Nils Anders Danielsson wrote a verified regexp matcher in Agda a while
ago.
http://www.cs.chalmers.se/~ulfn/darcs/Agda2/examples/AIM6/RegExp/
Although this isn't quite parsing, the ideas are relatively simple so
it's a good place to start. (Bob Harper has a theoretical pearl on the
topic, which might be worth checking out to get some inspiration).
More recently, Nils Anders has extended this to parser combinators
together with Ulf Norell:
http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-parser-combinators.pdf
Alternatively, you could explore how to implement similar ideas in
Coq. I'm a big Program fan and recently used it to verify some simple
programs in the state monad. I've just submitted a paper about this:
http://www.cse.chalmers.se/~wouter/Publications/HoareStateMonad.pdf
I'd imagine you might be able to take a similar approach to
applicative (or monadic) parser combinators. Doaitse Swierstra
recently wrote a good overview tutorial about parser combinators in
general that is certainly worth checking out:
http://www.cs.uu.nl/research/techreps/repo/CS-2008/2008-044.pdf
Hope this helps,
Wouter
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
