Community Z Tools 0.4 review

The Community Z Tools (CZT) project is building a set of tools for editing, typechecking and animating formal specifications written

License: GPL (GNU General Public License) File size: 0K Developer: Mark Utting and Petra Malik

0

The Community Z Tools (CZT) project is building a set of tools for editing, typechecking and animating formal specifications written in the Z specification language, with some support for Z extensions such as Object-Z and TCOZ. These tools are all built using the CZT Java framework for Z tools.

[Adapted from Andrew Martin's original CZT proposal] The Z specification language was adopted as an ISO standard in 2002. It 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.