Nitpick: A Checkable Specification Language
Author: Daniel Jackson
Proceedings of the Workshop on Formal Methods in Software Practice.
San Diego, January 1996
Download the PostScript.
Abstract
Abstract. Nitpick is a formal specification language designed to be amenable to generate-and-test checking, so that errors in specifications can be found automatically by systematic search. A compromise between expressive power and tractability was reached by limiting the language's datatypes, and not by eliminating features essential to abstract specification, such as implicit constraints and conjunction.