Nitpick is a tool for checking software specifications. You give it a specification along with a claim that the specification has some property. Nitpick evaluates the claim by searching for counterexamples. If it finds one, the specification does not satisfy the claim; if it does not, either the specification satisfies the claim, or Nitpick did not examine enough cases to find a counterexample.
Because errors can be missed, Nitpick is really a "specification debugger". But unlike conventional debugging and testing tools, Nitpick can examine billions of cases, so in practice it finds errors more reliably. And there's no need to specify individual cases to be tested. Instead you select a "scope" that bounds the size of the cases to be examined, and Nitpick generates all cases within the scope. Specifications and claims are written in NitpickUs own notation, NP. If you know a specification language such as Z, VDM or Larch, you should have no trouble learning it. If you already know Z, you'll find it even easier, since NP is almost a Z subset.
Nitpick can also perform a kind of limited simulation. It can generate instances of a state satisfying some invariants that you specify, or sample executions of an operation, even if you specified the operation implicitly.
Nitpick is the product of an ongoing research project at Carnegie Mellon University. Both the tool and the NP language are still under development; we expect big improvements in both in the next few years.
The NP language is not nearly as expressive as Z, and the tool can only handle small scopes. So don't expect to take a large existing specification and just run it through Nitpick. Think of an NP specification as a simplified model of the software you want to analyze, and the tool as a back-of-the-envelope calculator.
Despite its limitations, we think Nitpick is useful. It's the only tool we know of that can simulate implicit specifications and check properties completely automatically. We've found that it's much more fun writing specifications when you can simulate and check them as you go along. It's surprising how many errors you find this way.
Nitpick would make a nice teaching tool. The NP notation is much simpler than Z, and corresponds quite closely to the relational calculus. The interactive nature of Nitpick makes it easier to learn basic concepts, and to explore their subtleties in a way that is hard to do on paper. Students can use Nitpick to learn about sets, relations and functions; about invariants and relational specifications; and about theorems and counterexamples. The parts of Z missing would be higher-order types and the full schema calculus. We are beginning to develop course materials for teaching with Nitpick, and will be happy to share them with other educators.
For more information, contact
nitpick@cs.cmu.edu