Tools for Writing Formal Specifications Using Z Notation

by Alistair Miles

I learned some Z notation to write my masters thesis. I chose to use Z because I found it extremely helpful to be able to refer to a standardised mathematical notation; and because Z provides a number of conventions for grouping mathematical definitions, making reuse of definitions possible. Also, because the scoping rules are clearly defined, you can avoid ambiguity where variable names are reused within a specification.

Unfortunately I had no time to learn to use the traditional tool for writing Z specifications (latex) so I wrote my masters thesis using the math support in Open Office, adding new symbols for special Z characters. This partly defeats the purpose, because I couldn’t use a Z type checker to check variable type consistency within the specification.

Since then I’ve been experimenting with a number of tools for writing and publishing Z specifications, here are a few notes on what I’ve learned so far.

To author a Z specification in a WYSIWYG environment I’m using the jEdit plugin from the Community Z Tools project. Installing the plugin is a complicated and long-winded process, but I persevered, and I’m glad I did. The jEdit plugin includes syntax highlighting, syntax errors and type checking. It also performs conversion between three formats – UTF, latex and XML.

It is, however, somewhat fragile. When editing a document in UTF-8 format, the character used to end each declaration or schema is not visible, although if you step through the characters using the left or right cursor arrow you will notice an invisible character. If you don’t know this, you can very easily delete one of these characters accidentally, causing the document not to parse correctly. Also, many parsing errors are not reported in the error list – this means you quite often end up with a “not parsed” message in the ZSideKick plugin, with no error messages to explain why. In addition, I found that the use of a semi-colon to combine two universal or existential qualifications is not supported.

In short, the CZT editor works, but you have to spend some time getting to know it, and when it stops working it’s often not immediately obvious what’s gone wrong.

I also found an Eclipse plugin for Z based on the CZT code which is much easier to install. However, because the type checker is invoked continuously (rather than at save or manual refresh) eclipse slows down alot when specs go over a couple of pages – hence I’m sticking with the jEdit version for now.

Once I’ve written a Z specification using the UTF-8 format, I convert it to latex using the ZSideKick plugin for jEdit from CZT. Being a complete latex novice, I ran into a few problems getting from the latex markup to a PDF document. Here’s what I did. First I installed protext for windows. Then I installed the TeXlipse plugin for eclipse (1.1.0) and pointed texlipse at the miktex executables (Window > Preferences > TeXlipse > Builder Settings). Then I created a new latex project, with a single document using the “article” template. I copied and pasted the latex markup generated by CZT into the body of my new latex document. I then copied this “oz” latex style file into the project directory, and added the line “\usepackage(oz)” immediately after the documentclass declaration. Then building the document to PDF worked fine so far (although I’ve not tried every type of symbol or paragraph yet).

There are a number of available Z style files, but the thing to watch out for is that there are two major versions of latex, the earlier “2.09” and the more recent “2e”. There are substantial differences between the two versions, so Z style files for 2.09 will not work properly when built in a 2e environment. The style file I’ve linked from above works for latex 2e, which is what you get from the latest protext distribution.

As for generating HTML versions of Z specifications, I’ve had a go with the XSL transforms used by the WSDL 2.0 team (I contacted Arthur Ryman, he was very helpful). The problem with these is that they’re set up specifically for the W3C technical report format, and have a lot of baggage you won’t need for other purposes. I’ll have a go at factoring those out … one day 🙂

Advertisements