Data structures for Z testing tools.
Utting, 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.
Permanent Research Commons link: http://hdl.handle.net/10289/96
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.
University of Waikato, Department of Computer Science