Authors:Daniel Jackson and Craig A. Damon
CMU School of Computer Science Tech Report 95-216, November 1995.
Download the PostScript .
Executability is usually gained at the expense of implicit specification
constructs. This need not be the case. By identifying explicit elements
within a specification, and by employing reduction mechanisms to speed up
the search required by the implicit elements, it is possible to execute
specifications that are usually thought to be amenable only to proof. The
paper explains the basic notions behind the Nitpick tool, a checker and
simulator for specifications written in a relational language similar to Z:
the uniform representation of states, operations and claims as formulae;
the identification of derived variables by static analysis; and, briefly,
the underlying case enumeration method.
formal specification, operational specification, executable specification, prototyping, simulation, implicit definition, post-conditions, specification checking, relational calculus, Z.
Back to Nitpick Home Page