Hi Will,
I was wondering, Zeno capable of proving just equational statements, or
is it able to prove more general statements about programs? In
particular, it would be interesting if Zeno would be able to prove that
a function is total by verifying that it uses only structural
(inductive) recursion (on a well defined inductive type), i.e. each
recursive function call must be on a syntactic subcomponent of its
parameter. And dually, one might want to prove that a function is
corecursive, meaning that each recursive call is guarded by a
constructor.
Best regards,
Petr
Hi all, My masters project Zeno was recently mentioned on this mailing list so I thought I'd announce that I've just finished a major update to it, bringing it slightly closer to being something useful. Zeno is a fully automated inductive theorem proving tool for Haskell programs. You can express a property such as "takeWhile p xs ++ dropWhile p xs === xs" and it will prove it to be true for all values of p :: a -> Bool and xs :: [a], over all types a, using only the function definitions. Now that it's updated it can use polymorphic types/functions, and you express properties in Haskell itself (thanks to SPJ for the suggestion). It still can't use all of Haskell's syntax: you can't have internal functions (let/where can only assign values), and you can't use type-classed polymorphic variables in function definitions - you'll have to create a monomorphic instance of the function -but I hope to have these added reasonably soon. It's also still missing primitive-types/IO/imports so it still can't be used with any real-world Haskell code, it's more a bit of theorem proving "fun". You can try it out at http://www.doc.ic.ac.uk/~ws506/tryzeno, the code file given there has some provable properties about a few prelude functions among other things. Another feature is that it lists all the sub-properties it has proven within each proof. When it verifies insertion-sort "sorted (insertsort xs) === True" it also proves the antisymmetry of "<=" and that the "insert" function preserves the "sorted" property. Any suggestions or feedback would be greatly appreciated. Cheers, Will
signature.asc
Description: Digital signature
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
