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

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.