The Jaza Animator

Jaza is an `Animator' for the Z formal specification language.

It is intended to help you validate specifications via:

evaluating Z expressions;
testing Z schemas against example data values;
executing Z specifications (but not all specifications are executable).

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).

The following releases of Jaza (version 1.1) are available:

Binary Release 1.1 for Windows XP.
Binary Release 1.1 for Linux. This was compiled under Gentoo Linux, using GHC 6.2 with static libraries, so should also work on many other versions of Linux.
Source Release 1.1. This requires you to install Haskell first, either Hugs98 or GHC.

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 Windows.
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 paper (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).

marku@cs.waikato.ac.nz

Last modified: Fri Sep 16 11:56:38 NZST 2005