Using Oracle/SQL to animate Z specifications
Matthew L. Love · Formal Methods · 1992
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.