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

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

A summary of the main recent changes:

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).
Last modified: Fri Sep 16 11:56:38 NZST 2005