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. 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.
Product's homepage
What's New in This Release: [ read full changelog ]
· 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:
· 1. Click on the .jar file to open the CZT GUI.
· 2. Or do 'java -jar czt_1_5_0_bin.jar' to open the CZT GUI.
· 3. Do 'java -jar czt_1_5_0_bin.jar --help' to use the command line interface.
· czt_1_5_0_eclipse_plugin.zip is a CZT plugin for Eclipse 3.4. To install it, just unzip this .zip file into your top-level Eclipse folder (the one that contains the 'features' and 'plugins' directories), then restart Eclipse.
· The 'File / New / Other.../ CZT / CZT Project' command can be used to create a new CZT project, and then 'File / New / Z Specification' to create Z specifications. There is a CZT manual in the Eclipse 'Help / Help Contents' page.
· You should also install the following CZT font.
· CZTSans_1_5_0.ttf is a Bitstream Vera font with all the Unicode characters for Z added. You must install this on your system so that the Eclipse and jEdit editors can display the correct Unicode characters for Z. WARNING: on Windows systems this font may cause some Microsoft programs to crash - eg. Visual Studio Form Designer gives an illegal memory access error if this font is installed on the system.
· czt_1_5_0_src.zip contains all the CZT source files, including svn information. To compile it, you will need a recent version of Java and Maven. See the INSTALL.txt file for details.
Find us on Google+
