Overview

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, Circus, and TCOZ. These tools are all built using the CZT Java framework for Z tools.

Beta-versions of the end-user CZT tools are now included in the CZT releases (download). This includes a jEdit-based Z editor that gives WYSIWYG editing of the Unicode markup for Z, template-based insertion of Z constructs for LaTeX and Unicode markup, automatic typechecking on each save, a SideKick panel that shows the structure of your Z specification, conversion between the different markups and much much more. More information can be found in the manual. Here is a screenshot, showing some random Z in Unicode format:

CZT Tools within JEdit

Background

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

CZT Objectives

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 includes:

  • An XML Schema markup for Z.
  • Java classes for Z annotated syntax trees (AST).
  • Java classes for converting between XML and Java AST.
  • Java libraries for the common operations needed in every Z tool (markup-converters, parser, type-checker, etc.). A paper describing these has been presented at ZB2005.
  • Graphical Z editors, with facilities for easily entering the special Z unicode symbols. Currently we provide jEdit and eclipse plugins.
  • A Z animation tool called ZLive, with a customisable graphical user interface.
  • Export tools, to output Z in other notations or for other Z tools.
  • Extended versions of the libraries and tools to support Z extensions such as Object-Z and CIRCUS.