CZT Projects

It is based on the assumption that in the short term, CZT will be a loosely couple set of tools (like UNIX command-line tools), centred around an XML interchange representation for Z (Ian Toyn has a larger document which gives the rationale for this XML design). This XML format can include the informal text of specifications, and a wide variety of annotations, such as types and cross references links.

In the longer term, a Java representation of Z is desirable, because communicating via XML files is a very heavy-weight mechanism, and would be an inefficient way of linking a sequence of lightweight tools together. For example, in CADiZ, prelude.tex is 4141 bytes. Excluding informal text, prelude.utf8 is 792 bytes, but prelude.xml is 22212 bytes. Similarly, standard_toolkit.utf8 is 14093 bytes, and standard_toolkit.xml is 573670 bytes. So there is an overhead of roughly 20 times for XML, and that's with only some of the type annotations present.

Also, many projects are likely to want to write tools in Java, so it is desirable to have the AST (Annotated Syntax Trees) already defined in Java, with commands to convert them to and from the XML format etc.

Currently, CadiZ is the only Z tool that conforms to the Z standard, and Ian Toyn (the developer of CadiZ) is developing the XML format and has already implemented a prototype Z-to-XML translator in CadiZ v4, so the best way to get CZT off the ground seems to be to use CadiZ to parse, typecheck and translate specifications into the XML format. This will enable other tools to start using the XML format immediately.

The big question for Java-related tools is how much should they be based on Zeta? The AST of Zeta needs some changes to match the XML format more closely, and a few standard Z features are not supported by Zeta (for example, multi-word tokens and user-defined Delta and Xi schemas).

Proposal: We will use the infrastructure of Zeta, but define a new content type (AST) which corresponds closely to the CZT XML format. This has the advantages, including:

• the existing Zeta representation of Z (called ZIRP) will continue to work, along with all the existing features of Zeta (parser, typechecker, animator etc.). [If we instead modified the existing ZIRP to fulfill CZT requirements, they would break.]
• the new content type will be defined using standard Java, rather than Pizza, which will be more future-proof (perhaps) and certainly easier for students etc. to understand. [Wolfgang: Is it practical to avoid Pizza features while doing this?]
• the new content type will match the XML format exactly, and be uncluttered by the existing Zeta extensions.
• It should be possible to define a 'Adaptor' which converts the ZIRP Z representation into the CZT Z representation. This means that the existing Zeta parser and typechecker can be used to generate ZIRP Z, which will be automatically converted into CZT form when you request a CZT-specific operation, such as writing it to a CZT XML file.
• [If we could also define an adaptor for the reverse transformation, CZT to ZIRP, then we could use the Zeta animator on specifications loaded from XML files. However, I suspect that circular adaptor paths might be a bad idea. An alternative way of getting the same effect is to write the XML file out in the LaTeX markup, then load it into Zeta.]

More precisely, we will reuse:

• The Target = Unit x Content architecture, with Adaptors that translate one kind of Content into another.
• The GUI and command-line front ends (Session, Shell, Listener, message handling, Locator etc.).
• The Zeta.Util package which defines classes like Annotation, AnnotatedTerm, Name.
• The Zeta.Format package, which provides support for writing pretty-printers.

Possible projects [Ordered from sensible to wilder ideas]:

Z/Java Definition

Define Java data structures for Z, closely based on the XML DTD for Z.

Z/XML to/from Z/Java

Write a Java module that reads Z/XML format and converts it into the Z/Java data structures, and vice versa. These will use the standard Java XML library.

Standard Z to Z/Java input chain.

Eventually, we probably want Java versions of Z lexing, parsing, typechecking etc. This project will reimplement these, based on the markups defined in the Z standard, the grammar on Ian Toyn's web page, and the existing Zeta parser/typechecker chain.

Z/Java to Latex/Email/Unicode

Write Java modules for outputting Z/Java specifications in each of the markups defined in the Z standard. The LaTeX output will be useful for displaying Z.

Unfolder

Write a Java module that contains procedures for unfolding various Z constructs, such as the schema operators. This will allow other tools to start with a simplified form of Z if they wish.

DNF/CNF transformer

Write a Java module that can convert Z predicates/schemas into disjunctive/conjunctive normal form. This is a useful preprocessing step for several kinds of Z analysis.

Z Simplifier

Write a Java module that provides various routines for simplifying Z. The goal is to quickly simplify a Z construct before passing it to other tools, such as theorem provers. The simplifier would remove obvious redundancies (that typically result from other transformations), apply one-point rules etc. (Ideally, transformation tools like this and the above two should be generic, driven by a table of transformation rules that are written in a Z-like syntax, similar to the proof rules of CadiZ).

ZEUS Connection

Write a connection between ZEUS and Zeta, so that ZEUS can be used as the Z editor for large projects?

XEmacs Connection

Write/upgrade the Zeta to XEmacs connection so that specifications can be edited using XEmacs, in LaTeX markup.

Z Editor

Write (in Java) a simple WYSIWYG Z editor for students, similar to the Z/EVES editor?

Translators to provers.

Write translators from Z/Java into the input formats of various provers/systems, such as Z/EVES (accepts LaTeX or the Z/EVES XML format), Isabelle, SMV, Alloy, B etc.

TTF Test Case Generator

Write an interactive tool that implements the TTF (Test Template Framework) strategies for specification-based testing.

Refinement Condition Generator

Write a tool that, given two schemas, generates the proof obligations that check that one schema is an algorithmic refinement of the other.

Code Generator

Write a tool that, for a restricted subset of Z, generates executable (Java?) code for a schema.

Issues:

1. How should the Java (and XML?) structures support extensions of Z? More subclasses is the obvious way (in XML, extending/overriding the DTD). But some extensions may want to change one field within an existing kind of structure. This is probably best done by creating a new variant of that structure, to keep the extensions clearly separate from the standard.