Known "Z notation" applications ?

Question

I was just remembering back my university classes and was wondering to know if anyone out here even used the "Z notation" in a professional environment. I honestly must say that it was the single most boring class that I have ever attended in my life. Maybe because of the teacher, but at the time we really all thought it was a big waste of time. I might have been wrong, which is why I'd like to hear you about it.

If you are using it or some derived language (Z++), I'd just like to know how is it useful for you. Just curious to know some commonly-known applications of Z or your application.

For those who are not familiar : http://staff.washington.edu/jon/z/z-examples.html

Answer 1

I had to do Z back in uni! Brings back memories, if you have a Linux install handy try this application CADiZ...

Answer 2

I first encountered Z notation when I read that XCB (a replacement for the original Xlib API in X11) was proven correct with Z-notation .

Answer 3

It's worth looking at the B Method (http://en.wikipedia.org/wiki/B-Method). It's a slightly more pragmatic descendent of Z. The idea is that you can actually discharge a bunch of proof obligations through refinements steps (with the help of a theorem prover that is hiding behind the scenes) and then eventually generate code directly from your specification. I believe it has been used in a number of "real world" projects.

Answer 4

Z is (as you pointed out) a specification notation and not a programming language intended to faciliate formal verification.

One of the larger (publically known) projects specified using the notation was the protocol used in the Mondex smart card platform. There was recently a revival to determine the correctness of the original manual proofs with mechanical checking by multiple teams that included verification of the link text. Not surprisingly, no new fundamental errors were detected, although a number of assumptions were shown invalid by most of the teams.

Given the expressiveness of the notation it is unlikely that it will be extended. This would also make any proofs more complex and be counter-productive.

Answer 5

'Z++' is called object-Z. I haven't been active in Z since the early-'90s (working in part on a Windows port of CADiZ, which appears to have vanished), so have no idea if its current community, but some more recent papers have been published on using object-Z to formalise UML.