Software development: two approaches to animation of Z specifications using Prolog

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 in 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