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

sure..

[Anonymous Coward]

but when I transferred my algorithm into the system I made a small error.

so I designed a system that would convert C code into Z code. unfortunately I never did get around to fully debugging it, so I decided to write a theorem prover that would work on straight C code.

this one worked great, but one day it didn't catch a bug in some code that I *knew* was buggy.

so I decided to write another theorem prover to parse the code of the first one. I figured if I fed the code of each one into the other, that would greatly reduce the chances of error? well, the second one crashed at startup and the first one said it was correct.

turned out to be a bug in the OS. So I fed the OS source code into the first one, and it found some defects. I fixed the defects but then the system wouldn't boot any more. I think it was actually a bug in the C compiler, and I was going to fix it for real this time, but it was getting late.

so I decided to just try to write clear, simple code and fix bugs as they are reported.

Ahem

[eggstasy]

This is the 21st century my friend. Products aren't supposed to have a measurable amount of usefulness or quality. They are merely an excuse for other people to get their hands in your pocket.
Through comprehensive hyping and brainwashing (err, marketing) you could get a sizable amount of money out of selling a single turd. Ever heard of Merda d' Artista? It literally translates to "Artist's shit" and it IS shit. Very old shit but nothing more than human faeces. And yet, we are supposed to believe that it is a minimalist protest against the state of art (blah blah monocle polish yacht hampsters).
The thing sold for a bundle.

Spell checking?

[Godeke]

Ok, this may get me pounded, but I found this line amusing:

Z is a formal (i.e., mathematical) specification notation used by industry (especially in high-integraity systems) as part of the software (and hardware) development process

Perhaps they could include spell checking?

Sample Z source?

[Anonymous Coward]

The Z homepage is a frigging disaster.
What, pray tell, does Z code look like?