@device(postscript) @libraryfile(Mathematics10) @libraryfile(Accents) @style(fontfamily=timesroman,fontscale=11) @pagefooting(immediate, left "@c", center "@c", right "@c") @heading @heading(CMU-CS-96-109) @center(@b(Daniel Jackson, Craig Damon)) @center(January 1996) @center(FTP: CMU-CS-96-109.ps) @blankspace(1) @begin(text) Nitpick is a tool for checking software specifications. Like a model checker, it is fully automatic, but unlike most model checkers, it is designed for checking specifications of machines with complex state. HP, its specification language, is based on the relational calculus and is (almost) a subset of Z. The manual includes a guide to using the tool, and a description of the NP specification language. @blankspace(2line) @begin(transparent,size=10) @b(Keywords:@ )@c @end(transparent) @blankspace(1line) @end(text) @flushright(@b[(58 pages)])