[isabelle] Nitpick for Isabelle2009: Last Chance!



Dear all,

I've been continuously developing Nitpick---a counterexample tool
that, unlike Quickcheck, isn't restricted to executable formulas---for
about one year now. The latest version, with support for coinduction,
can be downloaded from

   http://www4.in.tum.de/~blanchet/nitpick.html

Nitpick has few users, but they seem happy. Here are some quotes:

   "Nitpick [hat] mir letzte Woche einige Stunden einspart, falsche
   Hilfslemmata zu zeigen."

   "I used the model generator Nitpick [...] to find a closure set
   of two SCGs, where none of them is sub-idempotent. [...] Nitpick
   rocks! Otherwise I would have actually written code just to
   enumerate stupid finite relations... Now I basically just had to
   write down the properties..."

   "What a fast tool. I've already installed it and am looking
   forward to the time savings it will surely provide."

   "We [...] are currently trying out the new Nitpick tool and it
   works very nicely with some of our theories."

The package contains everything you need. To install it, you just
need to type "./build".

We expect to bundle Nitpick with Isabelle starting with the next
official release, so this is your last chance to install Nitpick
manually and try it out.

Regards,

Jasmin






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.