The Jaza Animator
Jaza is an `Animator' for the Z formal specification language.
It is intended to help you validate specifications via:
Jaza is free, open-source software, distributed under the GPL (GNU Public
License). It was developed here at the University of Waikato, mostly
by me (Mark Utting). Development started mid-1999 and the current
version animates almost all of Spivey Z (2nd edition), except generics,
bags and axiomatic definitions.
Here is the Jaza User Manual and
Tutorial in PDF format (included in the distributions also).
- evaluating Z expressions;
- testing Z schemas against example data values;
- executing Z specifications (but not all specifications
The following releases of Jaza (version 1.1) are available:
A summary of the main recent changes:
- Jun 2005 (release 1.1): Improved evaluation of some function calls -- arguments are
now evaluated into canonical form before the function application.
This version has one known bug, when multiple exists at the same
level contain the same bound variable name. See the
README file for details.
- Mar 2005 (release 1.0):
The 'why' command now gives better
explanation about where and why evaluation was too difficult.
Numerous optimisation improvements so that more expressions
and schemas can be evaluated. In particular, nested exists within
schemas and set comprehensions are now unfolded then optimised.
- 28 Jun 2002: Alpha release of Z to BZP translators for Linux and
- 15 Apr 2002 0.90: Binary version now has command line editing.
(Source version provides command line editing if Hugs does,
but always handles backspaces). Extensive internal rewrite
to use the visitor design pattern. Schemas that contain false
are now optimized more agressively.
- 7 Dec 2000 0.86: several errors fixed, so that nested
\forall, \mu terms etc. are now more agressively optimized.
- 1 Nov 2000 0.84: vastly improved error messages.
Explicit bindings (\lblot..\rblot) are now supported.
The distributions include a user manual. Here is a
(also in PDF)
about the philosophy and implementation of Jaza, including
a small comparison with several other Z animators.
This paper was presented at the FM-TOOLS 2000 conference in Germany,
July 2000 (in TR 2000-07, Information Faculty, University of Ulm).
Last modified: Fri Sep 16 11:56:38 NZST 2005