Are You Using Z-Notation to Validate Your Software?

ghopson asks: "Many years ago in the early nineties I became aware of a software definition language called Z, which was based on set theory. The idea was that a software system could be defined in 'Z', and then that system could be mathematically proven to be 100% correct (in other words, zero defects).What is the current state of play with 'zero defect' software development? I know Z still exists, that there is a software development method (the B-method) associated with it. Have techniques and advances such as MDA advanced zero-defect software development? Or would a set of robust unit tests suffice?"

Comments

What is possible with Z

[NTDaley]

Some people here don't seem to understand the usefulness of Z.

When developing software the process might look something like this:
...
Specification (created with or by client)
Design
Implementation
Testing
...

Typically a specification could be a great big document written in english. It could have ambiguities, it could have subtle contradictions, it could be missing vital information.

If the specification is written in Z, then there are tools that let you:
- Find ambiguities or contradictions.
- Prove that some fact of the system necessarily follows from some other fact.
- Prove whether assumptions are correct.
- Test what results are possible given certain inputs and sequences of operations.

There are processes for, step by step, turning a specification into something more like real code, while proving that the two forms mean the same thing (apart from whatever limits are introduced). So, for example the transformed specification might change a variable from being an integer to being an integer in the range 0..65535, and you can test what effects this has.
All of this can be done before writing a single line of actual program.
Yes mistakes are still possible, but if done right, they are significantly less likely; and unlikely to be due to a misunderstanding about the capabilities of some part of the system.

Z can also help in the process of testing an implementation. From the specification you can see that, for example, the number 50 is the input value at which the behaviour of a function significantly changes, so you know to produce test sets checking the input of 50 and values on either side. This doesn't _have_ to be done by hand; my thesis supervisor is part of a project to automatically generate test sets from B and Z specifications.

So creating a Z specification:
-mean more work before coding starts (I think this is what makes most people uncomfortable with it :-)= ),
-forces you to be very specific about what correct behaviour is,
-allows you to test properties of the system before it is created,
-can help to make more useful test sets.

(Disclaimer: My Master's thesis involves making tools for Z, so I could be biased; but it also means I probably know more than average about Z).