Data Structures for Z Testing Tools

Abstract: This paper describes some of the difficulties and challenges that arise dur-ing 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 con-clude 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.