Here is a list of possible CZT projects.
Some should be suitable for student semester projects,
or larger honours/masters 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
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,
- The Zeta.Format package, which provides support for writing
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.
- 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.
- 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.
Last modified: Thu Mar 14 13:49:28 NZDT 2002