ZANS is an animation tool for Z specifications.
It is a research prototype that is still evolving.
The ultimate goals of ZANS are:
Currently, it supports the following features:
- Facilitate validation of Z specifications;
- Experiment design refinement and code synthesis
based on Z specifications;
- Assist learning of the Z specification language.
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
- type checking of Z specifications;
- expansion of schema expressions;
- evaluation of expressions and predicates;
- execution of operation schemas.
The documentation for ZANS tool includes a tutorial and a technical paper. Both are available online as follows:
These documents, soon, will be available in HTML format too.
- A Tutorial of ZANS:
- The technical paper: An Approach to Animating Z Specifications.
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.
For further information or if you wish to contact us, please send an email to email@example.com
Back to Group Page |
Updated on Feb 25, 1998