Abstract
This 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.