[Haskell-cafe] Parsing with Proof
muad
muad.dib.space at gmail.com
Tue Mar 31 17:31:36 EDT 2009
Hi everyone on haskell-cafe,
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 have an abstract syntax:
> data Parens = Empty | Wrap Parens | Append Parens Parens
assumption (A), in Append x y, x and y are never Empty
assumption (B), Strings only contain '(' and ')' characters
and a printing function
> print :: Parens -> String
> print Empty = ""
> print (Wrap m) = "(" ++ print m ++ ")"
> print (Append x y) = print x ++ print y
So the idea is that I would like to write parse :: String -> Maybe Parens,
such that if it gives Nothing then the String was malformed, if it gives
Just x then the string should be equal to print x.
I think I can write such a function in a few different ways, but I don't
know how to prove this code works, could anybody show me how?
Thank you for any replies.
--
View this message in context: http://www.nabble.com/Parsing-with-Proof-tp22814576p22814576.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
More information about the Haskell-Cafe
mailing list