Community Z Tools 1.5.0
Tools for editing, typechecking and animating Z specifications and related notations
[Adapted from Andrew Martin's original CZT proposal] The Z specification language was adopted as an ISO standard in 2002. The project can be used to precisely specify the requirements or behaviour of systems, and analyze that behaviour via proof, animation, test generation etc. However, one of the biggest barriers to the widespread use of the Z specification language seems to be the issue of tool support.
Many projects have constructed Z tools, some of product quality, most as student projects. Few of them are integrated with each other; few support all the new ISO standard; fewer still build together to form the kind of integrated environment that developers are beginning to expect.
Many good ideas have been developed to prototype stage, and then have been lost as projects have finished and students or researchers have moved on. The number of times a request for a Z parser arises in the Z newsgroup suggests lots of people are producing tools, most of which will never be seen outside their own institute. An integrated effort will move forward the state of tools, and thereby the take-up of Z.
Our objectives are to encourage interchange between existing Z tools (via a standard XML interchange format for Z), and to provide open-source libraries for building and integrating new Z tools. The software we are building does/will include:
1. An XML Schema markup for Z. See the ZB2003 proceedings for a paper describing this markup.
2. Java classes for Z annotated syntax trees (AST).
3. Java classes for converting between XML and Java AST.
4. Java libraries for the common operations needed in every Z tool (markup-converters, parser, type-checker, schema expansion etc.). A paper describing these will be presented at ZB2005.
5. One or more simple graphical Z editors, with facilities for easily entering the special Z unicode symbols. Initially we are using jEdit.
6. A Z animation tool called ZLive, with a customisable graphical user interface.
7. Export tools, to output Z in other notations or for other Z tools. (example, HTML output, LaTeX output, translation to B and JML).
8. Extended versions of the libraries and tools to support Z extensions such as Object-Z and TCOZ.
Community Z Tools
In a hurry? Add it to your Download Basket!
What's New in This Release:
- This release is a snapshot of all the CZT tools that are currently under development, including tools for the Z, Object-Z and Circus formal specification languages.
- czt_1_5_0_bin.jar is a binary release of CZT, which can be used as a GUI program or a command line program.
- For example: