On the animation of "Not executable" specifications by Prolog

An impediment to the widespread use of formal methods for software development is the difficulty in dealing with specifications, namely using them consistently in the software process. One approach to easing the management of specifications and improving their impact in the software process is animation, allowing developers to "execute" formal specifications as prototypes. This paper illustrates how Prolog can serve a multifaceted role for animating and prototyping specifications - as a target language, as the compilation/translation language, and to facilitate the advantages of formal methods through help in building formal proofs of properties such as correctness. Further, there is an implicit claim that, because of the correctness and directness of the translation, a subset of Z, not definitively established here, can be viewed as equivalent to a subset of Prolog.