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

Unit tests seem to be the way to go

[Jerf]

For the practical world, unittests seem to be the way to go. A large number of people have been experiencing very great and real success, without having to themselves be absolute geniuses to use.

Provable programs, on the other hand, are typically so complicated for a real-world program that your provably bug-free program still has bugs, because it turns out your model is wrong, because it was written by a human, not a god.

I'm very unimpressed with the whole "provable program" crowd for any but the most trivial proofs; decades of claims, little to show for it, and all based on the rather wrong idea that if we just push the need for perfection back one level, somehow the computer can magically take up the slack and prevent the bugs from ever existing. The unittesting philosphy, that bugs will happen and it's more important to test and fix them, since complete prevention is impossible anyhow, is much more based in reality, and correspondingly works much better in the real world.

(Provably correct computing is one of those branches of technology that may produce something useful, but is unlikely to ever acheive its stated "ultimate goals"; I class pure q-bit based quantum computing and pure biologically-grown computing in here as well.)

Re:Unit tests seem to be the way to go

[bigsteve@dstc]

If there does not exist a Turing Machine (read: 'program') that can decide in finite time whether a given program meets a correctness criterion, then we can never decide whether a program is correct, because Turing Machines are the best computational tools we have. Therefore, suppose some Turing Machine M exists that accepts as input some suitable correctness criterion, and a program, and outputs whether that program meets the correctness criterion (in finite time).

I believe that you are misunderstanding Rice's theorem (etcetera) and its consequences in an subtle, but very important way. I'll try to explain this in terms of the Halting Problem, because I think that people are more familiar with this.

The Halting Problem is to find a program P that takes two inputs Px and Ix. Px is an arbitrary program for a Turing-complete language, and Ix is an arbitrary input set for Px. Our program P has to return "true" if Px will terminate for input Ix, and return "false" if it won't. And it has to return the result in a finite time.

The Halting Theorem says that the program P does not exist. But what is more interesting here is what the theorem does NOT say. In particular, it does NOT preclude programs that will behave as required for a significant subset of Px X Ix. It also does not preclude programs that will return "true", "false" or "undecided" in a finite time. Finally, it says nothing about what proportion of the (infinite) space of Px/Ix combinations can (in theory) be proved to halt. Thus, we have the possibility that someone could write a very useful (though not universal) "halting tester" program.

Let's return to the bigger question of Rice's theorem and problem of proving programs correct. The key is the meaning of "algorithmically decideable". AFAIK, this means that there are no "universal" algorithms that can prove a non-trivial property about ANY program in a finite time. But (as with the Halting Theorem), it does not say that useful algorithms cannot exist, or what proportion of the space of programs these algorithms can (in theory) operate over.

obligatory quote

[Felipe Hoffa]

``Beware of bugs in the above code; I have only proved it correct, not tried it.''

Donald E. Knuth

Felipe Hoffa

Re:No!

[Anonymous Coward]

uhm, how will that function ever exit?

If this is true, call our function again.
If not, call our function again.

Ah crap, infinite recursion.

Requirements drift will kill you

[Beryllium Sphere(tm)]

In IBM mainframe land, there's a program called IEFBR14 designed to do nothing (don't ask, you DON'T want to know).

The usual story is that the first version had a bug report filed because, although it did indeed return, it didn't set the exit code.

Next, according to the conventional version, the linkage editor gagged because the source ended with an END directive instead of END IEFBR14.

With that fixed, the next bug report was that it didn't interoperate properly with the dump tools, in that it didn't stick the program name into a predictable area of the code.

Then came the bug report about chaining register save areas (again, you don't want to know -- it's related to the fact that the machines didn't have a stack).

Nor was that the end of it, a later bug report was that it wasn't being flagged as reentrant when it got linked.

That's five bug reports against a null program. All of them were integration problems and/or omissions in the specification.

There's a class of bugs formal methods can help with, but that class is a minority in most commercial work.

Re:what does this buy me?

[JohnFluxx]

Just to restate some of your points in a different way...

Z is an abstraction layer in the same way any specification is an abstraction layer.

You don't really want to ever go from what the user wants to C. Instead you have a design and specification. Then you validate that specification against what the user wants, code the C, and validate the C and specification.
This is done because it is easier to validate C against a written specification, rather than against some idea in the users head.

In the same way, in some cases it is easier validate the specification against Z, then validate Z against the C code, then validating directly.

I can't help but paraphrase Knuth's most famous phrase: Beware of this code for I have only prooved it to be correct, not tested it.

or something like that :)

Z.. haven't heard of that in a looong time

[Scorchio]

I studied for my CS degree at the University of York in the early 90's, who - at the time - were really pushing Z and Ada as the stuff of the future. One thing that stood out from the formal specification course, at least in my mind, was the example Z specification for a function to swap the values of two variables. Basically :

swap(a,b) :
tmp = a
a = b
b = tmp

The pseudocode is simple enough, but the Z spec took up a whole page. This put people off - if the smallest function in a minor subsystem of an application takes a whole page and much head-scratching to figure out, how long will the rest of the software take? Surely it's so time consuming as to be infeasible for real world use. Hardly any on the course really "got it", and I was one of the many who didn't. A friend of mine went on to use Z in his final year project, and at some point *ting* - he got it and found that it was good. I've never seen or heard of Z being used anywhere since, but some day I want to have another look at my notes and text books to see if it makes any more sense yet, and if so, whether it can help my work.

I don't know if they still advocate Z, but they started teaching Eiffel instead of Ada the year after I left..

Validation vs. verification

[Qoumran]

Great I just passed an exam in this, but lets see if I still remember it..

First you we have to get the question right - are you talking about validation or verification of software? They are quite different from each other:

• Validation: Are we building the right product?
• Verification: Are we building the product right?

The above is a quote of Boehm from 1979 I think... can't remember the exact title.

As you can propably guess there is quite a difference betweem the two. Unit testing is a method for verification, but from your description Z sounds like validation to me.

The killer problem with formal correctness

[metamatic]

Unless there's been some radical change in the state of the art that I've missed hearing about in the last few years, there's a big problem with Z notation and other methods of forming provably correct programs.

Said killer problem is that all the popular programming languages have features which make it impossible to model them using denotational semantics--that is, to produce mathematical functions which represent the program behavior. For instance, no C-based language can be modeled.

That's not to say that denotational semantics is completely useless. It's used in certain narrow domains, such as hardware--there are numerous chip designs where the circuitry and microcode is proven correct.

However, there's no way you're going to see --check-correctness flags on gcc or javac any time soon.

Of course, the bigger problem with mathematical techniques for proving correctness is that there's no measurable market demand for bug-free software (outside of the few narrow fields alluded to above), and hence no money available to spend on paying highly skilled computer scientists to spend a long time developing provably correct software using obscure programming languages. Instead, everyone just hacks together some alpha-quality code using C++ and calls it version 1.0.