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?

parser
type-checker
browsing/cross-referencing
specification management (configuration control, `sectioning' support etc.)
extension to Object-Z?
translation to and from various file formats: LaTeX, RTF, an XML representation
animation
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.

What now?

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