Introduction to the Z Word Tools
The Z Word tools are a collection of tools for editing, checking and using Z specifications within Microsoft Word. The tools include:
- styles for laying out schemas and other Z paragraphs;
- a Unicode font that includes all the Z symbols and is visually compatible with Times New Roman;
- automatic layout of Z paragraphs like the LaTeX equivalent, with italic text, formatted keywords and so on;
- the ability to enter symbols from a palette or (for died in the wool LaTeX hackers) typing in the markup;
- one-click typechecking, with errors highlighted in the Word document;
- generation of indexes and cross-references to definition and use of Z names;
- generation of diagrams showing the structure of the specification;
- the ability to hide the Z completely so the document can be used by maths-phobic readers;
- conversion of specifications written in Spivey Z to Standard Z.
This tool is also available as a separate Java download that can be used to convert LaTeX files on any operating system.
It can be used as a stand-alone program or as a Java class that can be incorporated into other tools, for example those based on CZT,
to allow them to process Spivey Z specifications. See the documentatation here.
- miscellaneous tools such as checking matching brackets.
The intention of the tools is
- to lower the barrier to the uptake of Z by removing at least one obstacle, the need to learn another document production method;
- to allow easy integration of Z with natural language, diagrams, tables and other notations relevant to the domain;
- to encourage incremental development of Z specifications by allowing frequent typechecking;
- to encourage the writing of good natural language by producing documents with the mathematics hidden.
tools support both the Z Standard and Spivey Z. Z
Standard specifications are processed with CZT and
Spivey Z specifications are processed with fuzz.
does not require declaration before use and works
across multiple documents: for example an operations
document can be checked against a separate data