Proposal: Community Z Tools Project (CZT)
One of the biggest barriers to the widespread use of Z seems to be the
issue of tool support. Many tools have been constructed, some of a
product quality, and most as student projects. Few of them are
integrated with each other; fewer still build together to form the
kind of integrated environment that developers are beginning to
expect. Many good ideas have been developed to prototype stage, and
then have been lost as projects have finished and students have moved
on. Many commercial projects have embodied huge amounts of research,
much of it lost when they have not made money in a suitable timeframe.
My proposal is to establish an Internet-based community project to build
first a framework/core for Z tool integration, and ultimately numerous plug-in
tools. The characteristics I have in mind are:
- Most of the tool-set would be open-source and freely available.
The aim is most definitely to come up with something that is larger
than any one project, student, company, or conference. It should
become sufficiently well-established that it persists even when
individuals move on. It should be open so that all manner of
students and other interested parties can write modules and
plug-ins, or indeed, improve upon the core. I would envisage the
core being under the GNU CopyLeft, with add-ons being licenced as
their authors may determine.
Why would people want to work on such a project? The number of
times a request for a Z parser arises in the newsgroup suggests
lots of people are producing tools, most of which will never be
seen outside their own institute. An integrated effort could move
forward the state of tools, and thereby the take-up of Z.
- It will be written in Java. This appears to be the best way to
support widespread use, and provide GUI tools. Java probably will
not give the performance necessary for automated proof tools, so
integration with other languages and systems may prove necessary.
- The (draft) ISO standard for Z will be the main reference point for
the core tools. This offers a good basis, is now relatively stable,
and expands the language from earlier treatments.
- This project would need to piggy-back on existing projects and
interest initially. I'd be very happy to seek funding for
development if anyone has good ideas about where it might be found.
Ideally, once there is a core established, all manner of people
might find it viable to contribute effort.
What kind of tools might be included?
- specification management (configuration control, `sectioning' support etc.)
- extension to Object-Z?
- translation to and from various file formats: LaTeX, RTF, an XML
- proof calculator/logical transformation tool
- automated proof tool
- link to existing tools
- tools for refinement to code
- integration with UML,
- experimental alternative logics (or conversion to B, VDM, etc.)
The core would provide elements of a toolkit for building these components;
classes and interfaces for Z semantic objects, panels for rendering them to
the screen, etc. etc.
I plan to post this proposal to comp.specification.z a couple of times
in the next six weeks. I would be interested to hear both positive
and negative feedback. They might be accompanied by offers of support
or resources, existing code, etc. By all means, discuss the ideas
in the newsgroup too if you wish to.
If there is sufficient support, the next stage would be for a group to
produce a project plan, describing arrangements for the project
framework and standards, and criteria for review and release of
software. This would be quickly followed by a design for the core
components, made available for public review. This would include a
high-level description (in Z?) and some key implementation pointers.
People might start to build prototypes.
Thereafter, coding might proceed at various sites, with a central
repository and periodic incremental releases.
A P Martin
Last updated: 25th September 2001