Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Will Sonnex <ws506 <at> doc.ic.ac.uk>
Subject: ANNOUNCE zeno 0.1.0
Newsgroups: gmane.comp.lang.haskell.general
Date: Sunday 31st October 2010 16:35:08 UTC (over 6 years ago)
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
 
CD: 3ms