Slashdot Mirror
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?"
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.
Perhaps they could include spell checking?
Sig under construction since 1998.
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.)
Your question is about Formal Methods. This field in computer science seems more popular in Europe than in the US theese days.
Two good articles you should read :
If your question was about their use in practical projects in industry, I've heard recently of teams doing serious work for Airbus (safety-critical embedded software using either B or Esterel) or for Gemplus (entirely proven JVM for javacards using B).
ACL2 is a theorem proving and modeling environment, based on Common Lisp, which is used for verification of hardware and software. I believe AMD used it to prove the correctness of the floating-point division algorithm in one of their processors.
Bush Lies Watch
In other words, I can prove that if my software is 100% bug-free, it's bug-free. Woohoo. This doesn't address the case where my program doesn't fully conform to the Z specification, does it?
In formal verification, the idea is that you would have a way to prove the equivalence between your Z model (or whatever modeling language you use) and your implementation. Of course, it's a lot more difficult to prove equivalence between a formal model and a C implementation, than if you are using a modern high-level language like Standard ML.
Bush Lies Watch
both robust unit testing and formal methods have their place --- formal methods for proving design and unit testing for proving implementation. however, it seems to me that the question of why formal methods aren't more widespread in the us boils down to a question of perceived cost v. perceived benefit. let's say it takes "n-nines" of reliability to keep enough of your customers satisfied enough to keep coming back to you. let's say you've got two designs for software which accomplishes a certain task, and both models (if implemented correctly) would result in a product that the customer would be sufficiently happy with. which model do you implement? odds are mostly likely that you'll go with the cheapest one, because that's what maximizes profits. (forget everything i just said if you are an academic or coding for the love of it). to borrow a line from an engineering prof: "perfection is the enemy of good enough, and it's good enough that sells"
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).
bits and peace
Nicholas Daley
Actually, I think the real kicker is the inverse of the problem you describe. It may very well be possible to prove that your C program properly conforms to the Z model. But is your Z model correct?
For many real-world problems, figuring out *exactly* what you want your program to do in all situations (and figuring out what all the situations are in the first place) is the hard part. You can then go implement that in C almost as easily as you can in Z.
I'm not saying this (Z and B) is useless. I just want to focus on the real problem. Using a modeling language just introduces one additional layer of abstraction into the process. While this may make the system easier to discuss and easier to "prove correct", it also introduces another layer at which errors may creep into the system. For some cases, the extra layer introduces fewer errors than it prevents. For other cases, the opposite is true.
I think to some extent it comes down to "how much time are we going to spend making sure this software is darn near perfect." The law of diminishing returns says that the number of flaws fixed per unit of programmer time will go down as more programmer time is applied, providing a "cost to flaw" curve. Customers also have a curve of how much they are willing to pay for additional reliability. The curves meet at some price point/quality level (keeping features constant), and that is where the product will ship. If the customer's need for extra reliability is large enough that the modeling phase can be integrated properly into the product schedule, it becomes worthwhile to spend time with formal models; otherwise, these will only decrease reliability since the modeling phase eats into the time needed for other phases to properly implement the product.
In other words, I think that a formal modeling phase is overkill for most requirements ("doesn't crash too often") since it has less bang for the buck as far as generating features and fixing glaring bugs. But it continues to have at least some bang for the buck long after other processes drop off in effectiveness. So it is worthwhile to add formal modeling when unit testing isn't going to get you to your desired flaw rate.
Time flies like an arrow. Fruit flies like a banana.
There are points at which you have to help the software along, tell it which strategy to use, or give it a half-way point to prove first.
If the assumptions being tested are provable, then it is valid to make those assumptions. If you can't prove them, then you don't really know that they are correct, and you shouldn't be making them.
Some pieces of code it is possible to prove whether it halts or not. It is possible to prove that:
while(true);
does not halt.
It is possible to prove that:
for(int i=0;i<10;i++)cout <<i<<endl;
does halt.
Similarly, as you say, there are other facts it is not possible to prove about a system. However if these facts need to be true for your system to be working properly, and they can't be proved, then there is something wrong with the system. e.g. If it is not possible to prove that your hello world program outputs "Hello World!", then it should be rewritten/fixed so that this can be proved. Otherwise the program is faulty, and may not do its job.
bits and peace
Nicholas Daley
``Beware of bugs in the above code; I have only proved it correct, not tried it.''
Donald E. Knuth
Felipe Hoffa
I vaguely remember that short of an exhaustive date set test, it's actually IMPOSSIBLE to determine mathematically that an algorithm is correct for any but the simplest (read shortest) pieces of code.
/* terminate and return 1 for any positive input */ ... are really, really hard to prove correct. In general, it's not feasible to prove big pieces of practical code correct using techniques like these, but with suitable abstraction it can be a helpful part of the engineering process. In any case, it is definitely not impossible.
This is total crap. You can, of course, prove algorithms of any size correct. Some really long (textually) algorithms can be easy to prove, and some really short ones, like this:
int collatz(int i) {
if (i & 1) return collatz (i * 3 + 1);
else return collatz(i >> 1);
}
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.
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
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..
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:
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.
--- Martin Skøtt aka. Qoumran
But there is certainly no theorem telling us that it's hopeless.
Yes, there is. Rice's theorem proves it impossible in the general case. And in fact, the very fact that you can produce a proof of correctness tends to argue not that your proof is powerful, but that the algorithm, even if it looks fancy on paper, is trivial. The proof system is necessarily less powerful then the computational system; see Godel's theorem.
And all the such proofs I've seen, while very useful in the real world (it's vital to prove your sorting routine is correct) are of effectively trivial routines.
Basically, the existance of a proof is a certificate of triviality. Mercifully many trivial algorithms are still wonderfully useful, like hashtable algorithms and sorting algorithms. But once you want to do something useful, like accept user input and do something, you can't just string together all of the proven correct algorithms and get another proven-correct algorithm; as the algorithm leaves the domain of "sort this list" or "find the shortest path" or even "find the minimal flow from the source of the graph to the sink of the graph" (an interesting problem who's best-known solution has gone from O(n^5) to O(n^3) over the years, which is really cool) into a couple hundred of these things strung together in arbitrary combinations, your proof system necessarily breaks down.
I'd go on, but this is already below the front page fold by five or ten pages, so who'd read it anyway?
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.
GCHQ Quantum Insert installed. If only our tongues were made of glass, how much more careful we would be when we speak
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).
I've heard of a different idea. Once you define the problem in this language called "C", the software is automatically written by this device called a "compiler", and it is already proven to be 100% correct.
Bart Massey and Jamey Sharp of Portland State have written XCB, a reimplementation of Xlib with an eye towards improved tunability (and an improved API). They were having problems coming up with an implementation that worked properly; the multi-threaded connection handling code was up to four designs and two implementations, all of them incorrect.
- zxcb.pdf
Massey and Robert Bauer of Rational ended up writing a Z specification for that portion of the code, and proved it correct. The C implementation of the spec is in the XCB distribution right now.
Massey and Bauer published a paper describing this effort for USENIX 2002. They conclude with the comment "[t]he sort of lightweight modeling described [above], that isolates a troublesome portion of the system for more detailed study, is especially appropriate[...]".
XCB Wiki: http://xcb.wiki.cs.pdx.edu/
XCB/Z Paper: http://xcb.wiki.cs.pdx.edu/pub/XCB/WebHome/usenix
Yes, there is. Rice's theorem proves it impossible in the general case.
You are misapplying the theorem, or else don't understand what it says. There are systems where given a program, and a proof, verification of non-trivial properties (like termination) is decidable. Yes, there is no program that will generate that proof for you for arbitrary programs and properties. But that does not mean that a human (or even, sometimes, a computer) can't create a proof for a specific program and then verify that proof mechanically. People do that every day, and it does not mean that the properties are trivial, either in the Rice sense or the practical sense.
The argument you're making is essentially identical to, "The undecidability of the halting problem tells us that writing programs is hopeless." Making general program-writing tools (input spec, output program) is hopeless, yes, but that does not mean that we can't make lots of useful specific programs.
I'd go on, but this is already below the front page fold by five or ten pages, so who'd read it anyway?
I will.
In the short term I'm not persuaded by the case for widespread application of formal methods, but in the long run I think it will become very important. Two areas I think are areas that I think are most beneficial for formal methods: firstly verified implementations of network protocols, and journalling file systems.
I don't mean to be glib by making such a statement as "software is still voodoo", but after reading this thread, it is quite obvious I think that clear understanding of our art is achieved by far too few practitioners, and that is the crux of the problem of software quality.
While provably correct solutions are presently unrealistic, we have myriads of tools to assist in the process of creating high quality software. Specification tools like Z, modelling languages, coverage analysis and profiling software, unit testing and regression prevention methodologies, runtime assertions---all are proven to increase and control quality. Moreover, language constructs such as taxonomic class hierarchies with crisp declarations can prevent many logical or semantic flaws at compile time, but only if used by class designers who understand good architecture and the importance of minimizing conceptual baggage and side-effects.
Yet, I live in a world where I regularly encounter professional developers who do not use version control and move from idea to implementation quickly without adequate (or sometimes without any) specificiations at all. These are not amateur hackers, but well-paid professionals who happen to be working on websites which accept credit cards and banking details, among others.
While many of us can understand and use quality-assurance tools and processes, there are just as many (perhaps more) that rely solely on their intuitive ability to "sling code", and worse, are arrogant in their belief that time spent in formal specification and analysis is a waste of time.
Arguing that particular specification tools are useful is fine, but don't entertain for a moment the belief that the larger problem of software quality is even vaguely related to a lack of theoretical foundation for quality. The theoretical foundation is alive, well, and rich with solutions.
The problem is people, education, and professional standards.
Until there are employment and "best practice" requirements for software engineers which are as rigorous and well-accepted as those for other engineering disciplines, we will continue to unacceptably low quality in the software we use, with an incredible corresponding waste in time and human effort.
I used Z to design the control software for a radiation therapy machine.
I expressed the safety requirements in Z, and also expressed the detailed design in Z, and argued (I wouldn't say "proved") that the design didn't violate the safety requirements.
We coded the control program in C from the detailed design in Z. Of course we tested the program thoroughly too - you still have to do all that, of course.
The machine has been in use treating patients since July 1999. We haven't killed anyone yet (unlike some other products in this category).
There are some papers and reports about the project at
http://staff.washington.edu/~jon/cnts/index.html
There is a short (3-page) report about our use of Z in this project at
http://staff.washington.edu/~jon/cnts/iccr.html
There is a longer report about the whole project at
http://staff.washington.edu/~jon/cnts/cnts-report. html
The Z for the radiation therapy machine itself is at
http://staff.washington.edu/~jon/z/machine.html