ON THE ANIMATION OF “NOT EXECUTABLE” SPECIFICATIONS BY PROLOG
- 1 March 1996
- journal article
- Published by World Scientific Pub Co Pte Ltd in International Journal of Software Engineering and Knowledge Engineering
- Vol. 6 (1) , 63-87
- https://doi.org/10.1142/s0218194096000041
Abstract
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.Keywords
This publication has 0 references indexed in Scilit: