Z Animation in Zans

The intention in animation of a Z specification is to provide an automated means to verify the veracity of the specification. This includes resolving questions such as:

. does the Z specification conform to Z syntax and type rules?

. is the specification coherent (i.e., logically sound)?

. is each of the stated invariants and post-conditions a logical consequence of the pre-conditions?

. does the formal specification really guarantee the desired behavior of the system under consideration?

Animation systems based on one of two approaches have been developed to automate the verification process. One depends on an area of artificial intelligence -- automated deduction (or mechanical theorem proving). In this approach a program is employed that attempts to carry out the logical deductions indicated above. While such systems have proven of use in numerous cases, the current state of research in automated deduction is unable to support broadly usable systems -- sometimes an automated prover may fail to find a proof of a true assertion. Links to examples of such systems can be found on our course Web page.

The Zans system we are using is based on an alternative methodology. In this approach, a model of the specification is constructed for which each of the invariants and pre-conditions is true, and then the post-conditions are evaluated to see if they are also true. If not, then the specification clearly is incorrect. However, even if the post-conditions are true in this one model, that does not preclude the existence of another where they are not. Users of the system can direct the construction of numerous models to be explored, but can never be assured of the absence of errors. However, such systems can reliably check syntax, types, etc. In the majority of such systems a mathematical type setting system is employed to deal with the esoteric Z syntax. Zans is unique in providing an alternative syntax expression for Z using only the readily available ASCII character set. See our class directory for Diller's phone database system expressed using Zans, and for a script illustrating its use.