Using Oracle/SQL to animate Z specifications

Reports on the use of Oracle, an industry standard relational database CASE tool, as an environment for animating suitable Z specifications. The basic method of the animation is to encode each schema of a Z specification as a `form´ which can be displayed on the screen. The user may enter values into the input fields, but the state values are only updated if `triggers´ which encode the specification´s predicates so permit. The user may execute a sequence of forms to explore the effects of composing a number of operations. The animation may also highlight missing or contradictory logic in the original specification