CZT Eclipse IDE
Develop Z specifications in Eclipse-based Community Z Tools IDE: parsing, typechecking, verification condition generation and more!
CZT Eclipse features
Numerous IDE features to assist with Z specification development: content assist, syntax colouring, Z character input, document outline, etc.
Z/EVES Eclipse
Z/EVES Eclipse provides a modern integration and prover IDE for the Z/EVES theorem prover.
CZT for Eclipse
Community Z Tools provide plug-ins for Eclipse IDE that integrate Z specification development tools in a modern IDE.
The aim is to provide a comprehensive development environment for formal specifications written in Z and Z dialect notations, from typesetting to verification. Eclipse provides a convenient platform to put core Community Z Tools into action and deliver formal development tools to users.
Download
CZT Eclipse is available both as standalone Community Z Tools IDE and as plug-ins for Eclipse to be installed via Update Manager.
Refer to the Download page for details.
Features
CZT Eclipse aims to provide a development environment for Z specifications. Some of the available features are listed below.
-
Continuous typechecking: the Z specification is automatically checked during editing and any issues are highlighted in the document.
- Select Z dialect to use for parsing and typechecking specification in the preferences.
-
Content assist
-
Verification condition generation: generate verification conditions (theorems) for the active specification and insert them into the specification.
-
CZT font: a font supporting special CZT characters is loaded and used automatically for Z Unicode specifications.
-
… and more!
Read more about the CZT Eclipse features in the documentation.
Z/EVES Eclipse
Community Z Tools also provide an integration with the Z/EVES theorem prover within the Eclipse IDE. Learn more at the Z/EVES Eclipse page.