Alistair Miles

Category: z notation

Formal Specification of RDF Concepts

I had a go at rewriting the RDF Concepts and Abstract Syntax as a formal specification using the Z notation, to try out the CZT editing, type checking and format conversion tools. The files I’ve produced so far are linked below:

I wrote the specification in plain text UTF-8 format, using the jEdit plugin from CZT. I then used the CZT tools to convert to latex format, which I had to edit a bit before I could get to a nice looking PDF. I haven’t tried to get to HTML yet, I’m saving that for a rainy day 🙂


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 »