This software provides a set of tools for editing, typechecking, and animating Z specifications and other related notations.
The Community Z Tools (CZT) project is a set of tools designed to edit, typecheck, and animate formal specifications written in the Z specification language. It also provides some support for the Z extensions such as Object-Z and TCOZ. All of these tools have been built using the CZT Java framework, which is specifically designed for Z tools.
The Z specification language was standardized as an ISO standard in 2002. With the CZT project, users can precisely specify the requirements or behavior of systems and analyze that behavior via proof, animation, and test generation. However, the lack of proper tool support remains a significant barrier to the widespread adoption of the Z specification language.
Numerous projects have tried to address this issue by constructing Z tools, but most of them are either of product quality or created as student projects. Integration between tools is rare, and even fewer tools support all the new ISO standards. This fragmentation has resulted in many good ideas being lost as projects finish and researchers move on.
Therefore, the CZT project aims to encourage the interchange of existing Z tools by providing a standard XML interchange format for Z. It also aims to develop open-source libraries for building and integrating new Z tools. The software built by the CZT project includes an XML Schema markup for Z, Java classes for Z annotated syntax trees (AST), and Java classes for converting between XML and Java AST.
Additionally, the CZT project provides Java libraries for the common operations needed in every Z tool, such as markup-converters, parser, type-checker, schema expansion, etc. There are also various graphical editors, including a simple graphical Z editor with facilities for easily entering the special Z unicode symbols, as well as a Z animation tool called ZLive with a customizable graphical user interface.
Export tools are also available to output Z in other notations or for other Z tools, such as HTML output, LaTeX output, translation to B and JML. Finally, the CZT project offers extended versions of libraries and tools to support Z extensions like Object-Z and TCOZ.
Overall, the CZT project provides an integrated environment for developers and fulfills the need for better tool support in the Z specification language.
The Z specification language was standardized as an ISO standard in 2002. With the CZT project, users can precisely specify the requirements or behavior of systems and analyze that behavior via proof, animation, and test generation. However, the lack of proper tool support remains a significant barrier to the widespread adoption of the Z specification language.
Numerous projects have tried to address this issue by constructing Z tools, but most of them are either of product quality or created as student projects. Integration between tools is rare, and even fewer tools support all the new ISO standards. This fragmentation has resulted in many good ideas being lost as projects finish and researchers move on.
Therefore, the CZT project aims to encourage the interchange of existing Z tools by providing a standard XML interchange format for Z. It also aims to develop open-source libraries for building and integrating new Z tools. The software built by the CZT project includes an XML Schema markup for Z, Java classes for Z annotated syntax trees (AST), and Java classes for converting between XML and Java AST.
Additionally, the CZT project provides Java libraries for the common operations needed in every Z tool, such as markup-converters, parser, type-checker, schema expansion, etc. There are also various graphical editors, including a simple graphical Z editor with facilities for easily entering the special Z unicode symbols, as well as a Z animation tool called ZLive with a customizable graphical user interface.
Export tools are also available to output Z in other notations or for other Z tools, such as HTML output, LaTeX output, translation to B and JML. Finally, the CZT project offers extended versions of libraries and tools to support Z extensions like Object-Z and TCOZ.
Overall, the CZT project provides an integrated environment for developers and fulfills the need for better tool support in the Z specification language.
What's New
Version 1.5.0: N/A