Software development: two approaches to animation of Z specifications using prolog
- 1 January 1992
- journal article
- Published by Institution of Engineering and Technology (IET) in Software Engineering Journal
- Vol. 7 (4) , 264-276
- https://doi.org/10.1049/sej.1992.0027
Abstract
Formal methods rely on the correctness of the formal requirements specification, but this correctness cannot be proved. This paper discusses the use of software tools to assist the validation of formal specifications and advocates a system by which Z specifications may be animated as Prolog programs. Two Z/Prolog translation strategies are explored; formal program synthesis and structure simulation. The paper explains why the former proved to be unsuccessful and describes the techniques developed for implementing the latter approach, with the aid of case studies.Keywords
This publication has 6 references indexed in Scilit:
- Foundations of Constructive MathematicsPublished by Springer Nature ,1985
- Prolog as a Language for Prototyping of Information SystemsPublished by Springer Nature ,1984
- Foundations of Logic ProgrammingPublished by Springer Nature ,1984
- Programming in PrologPublished by Springer Nature ,1984
- Numbers, Sets and AxiomsPublished by Cambridge University Press (CUP) ,1983
- Elements of Recursion TheoryPublished by Elsevier ,1977