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:

1. styles for laying out schemas and other Z paragraphs;
2. a Unicode font that includes all the Z symbols and is visually compatible with Times New Roman;
3. automatic layout of Z paragraphs like the LaTeX equivalent, with italic text, formatted keywords and so on;
4. the ability to enter symbols from a palette or (for died in the wool LaTeX hackers) typing in the markup;
5. one-click typechecking, with errors highlighted in the Word document;
6. generation of indexes and cross-references to definition and use of Z names;
7. generation of diagrams showing the structure of the specification;
8. the ability to hide the Z completely so the document can be used by maths-phobic readers;
9. 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.
10. 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.

The tools support both the Z Standard and Spivey Z. Z Standard specifications are processed with CZT and Spivey Z specifications are processed with fuzz.

Typechecking does not require declaration before use and works across multiple documents: for example an operations document can be checked against a separate data model document.