Utting, Mark2008-03-192007-07-222008-03-192001-06-01Utting, M. (2001). Data structures for Z testing tools. (Working paper series. University of Waikato, Department of Computer Science. No. 01/4/2001). Hamilton, New Zealand: University of Waikato.https://hdl.handle.net/10289/96This paper describes some of the difficulties and challenges that arise during the design of tools for validating Z specifications by testing and animation. We address three issues: handling undefined terms, simplification versus enumeration, and the representation of sets, and show how each issue has been handled in the Jaza tool. Finally, we report on a brief experimental comparison of existing Z animators and conclude that while the state of the art is improving, more work is needed to ensure that the tools are robust and respect the Z semantics.application/pdfenWorking Paper