A LISP-based environment for animating Z specifications

Summary form only given. ZAL (Z Animation in LISP) is a package of extensions to Common LISP which allows a Z specification to be incrementally designed and validated in an interactive environment. A Z specification is transformed into an equivalent ZAL program which can be executed in order to demonstrate the functionality of the intended implementation. The aim has been to ensure that the transformation rules are simple and mechanical, so that the ZAL version is essentially a rewrite of the original Z. A substantial subset of the Z notation has now been implemented in ZAL, and the package has been used to animate a collection of non-trivial Z specifications. A full-screen editor for Z has also been implemented as a basis for a front-end which will ultimately hide the underlying LISP notation from users of the system. Not only does the package provide facilities for users to validate their own specifications, but it interactive nature also encourages and supports an experimental approach as a valid technique for the development of Z specifications