Email Gateway (Aug 18 2022 at 14:05): Email Gateway (Aug 18 2022 at 14:05):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
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
Last updated: Nov 21 2024 at 12:39 UTC