Semi-Executable Specifications

Authors:Daniel Jackson and Craig A. Damon

CMU School of Computer Science Tech Report 95-216, November 1995.

Abstract

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.

Keywords:

formal specification, operational specification, executable specification, prototyping, simulation, implicit definition, post-conditions, specification checking, relational calculus, Z.

Back to Nitpick Home Page