Tools for Writing Formal Specifications Using Z Notation

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.

Read the rest of this entry »