display | more...

There's a whole lot that could be written here, but I'll keep it short(ish). A Z specification is a formal model written using the Z notation. By formal model, I mean a model written in a notation based on some branch of mathematics.

The first thing about a Z specification is that it is a collection of Z schemas. Well, it's more than that. A lot more than that. Tony Hoare once said that the most important part of a Z specification was the natural language text that surrounds it.

That statement is almost revolutionary; he's saying that (in my case) the English text I write around the schemas is more important than the schemas themselves. If that's the case, why bother performing all the hard work of writing down the Z specification? My answer to that is that I can't write the English text, and be precise about it, until I've understood the thing I'm specifying and I can only gain that understanding after I've modeled the thing.

There's another reason to support his statement: humanity has spent many millennia learning how to communicate through use of natural language and not nearly as long communicating through mathematics!

The bottom line is that the English language text gives you the intuition about the model (well, it does if it is well written) and the mathematics gives you the precise model.

You can, with a little imagination, write a Z specification of pretty well anything! Some time back (around the mid 1990s) I was involved with the development of a POSIX standard - specifically POSIX 1003.21, a standard for an interface for real-time distributed systems communication. When I joined the group, they had a requirements specification written in English which I modeled in Z. The act of building the model was interesting and forced me to examine the requirements closely and, happily, raised a number of issues which the rest of the committee was able to correct. The specification itself included a lot of text stretching to a total of 70 pages, of which 50 pages were explanatory and 20 pages were schemas! Modeling the requirements and communicating the results of that model back to the committee helped improve the standard.

<boast mode>I was told that some years later a researcher had compiled a list of the publicly known Z specifications and that mine took the record for being the largest</boast mode>. If you want to read mode examples, there's a nice book by Ian Hayes called "Specification Case Studies". It's old, but that doesn't mean it's not worth reading.

Side note: I was told that there was a debate in Oxford as to the correct plural of schema. Technically, since schema is a Greek word, its plural would be schemata. But, in English, schemas is also acceptable. I was told that the decision came down to schemas simply because schemata would sound too pretentious. I suspect, though, that they already knew that most people would use schemas, so why fight it! I'm sure the Greek purists weren't happy, but that's their problem not ours.