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?"
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
Someone also needs to tell this crowd that some bugs are result of implementation itself. Out of bounds, errors, looking in non-existent resources, etc. Of course exception handling mechanism should be used where appropriate but that itself is prone to programmatically mistakes.
Unit Testing is by far the best way to go. You find a problem, you fix it but at the same time make sure you don't introduce new problems. This might seem like a daunting task when dealing with a large system but it sure beats trying to strive for perfection all at once.
Test, test, test I say.
-----
One is born into aristocracy, but mediocrity can only be achieved through hard work.
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"
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);
}
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?
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
C is not a language for the timid :) Case in point: A really interesting hole in the C/C++ spec
that nails programmers is the interaction between side effects and sequence points. Which, long story short leaves statements such as: Fx(y++, z=y), undefined. The compiler only guarantees that side effects will have been completed at the next sequence point, the compiler could choose to evaluate the operators in either order and be in complete compliance.
Religion is a gateway psychosis. -- Dave Foley
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.