Z ANIMATIONS
Introduction
ZANS is an animation tool for Z specifications.
It is a research prototype that is still evolving.
The ultimate goals of ZANS are:
- Facilitate validation of Z specifications;
- Experiment design refinement and code synthesis
based on Z specifications;
- Assist learning of the Z specification language.
Currently, it supports the following features:
- type checking of Z specifications;
- expansion of schema expressions;
- evaluation of expressions and predicates;
- execution of operation schemas.
A Z specification prepared for ZTC can be animated by ZANS withlittle or no modification.
ZANS supports the Z syntax defined in the second edition of ZRM
Documentation
The documentation for ZANS tool includes a tutorial and a technical paper. Both are available online as follows:
- A Tutorial of ZANS:
- The technical paper: An Approach to Animating Z Specifications.
These documents, soon, will be available in HTML format too.
Download site
The platforms supported are listed below. For each one of these, the complete set of files for ZANS tool, which includes examples, documentation files and precompiled executables can be downloaded by clicking one of the links:
Please, when you download the tool, fill in the electronic registration form
and submit it, so you can receive automatically any information regarding
updates, bug fixes etc. The registration form can be found in Registration page.
Contact Info
For further information or if you wish to contact us, please send an email to fm@saturn.cs.depaul.edu
Back to Group Page |
SE Home
webmaster@saturn.cs.depaul.edu
Updated on Feb 25, 1998