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.

Re:sure..

[Anonymous Coward]

Uh... I studied the halting problem some 5 or 6 years but I can't see how it relates to that person's post. Could you elaborate?

Re:sure..

[Anonymous Coward]

hes just trying to get the mods that dont know what it is to mod him up. ignore him

Re:sure..

[tigersha]

If he does what he claims to have done he would need to solve the halting problem. Theorem provers can usually check theorems (this is possible) but to prove theorems them you need to solve the halting problem. There are heuristics that can do quite OK, but on a complicated thing like a C compiler and an entire OS they will choke. Most theorem provers AFAIK are more like proof assistants in that they can prove the boring drudgery but the deep "aha" steps still need to be human. However, sometimes the prover can check that the proof of the aha (human supplied) is correct.

I knowe one theorem prover proved with human help Goedel's incompleteness theorem and if they can manage that they should manage quite some deep things, but it was still a human assisted.

However, the poster's point is valid. In order for your program to work correctly all the infrastructure that runs around it, including OS/libraries/network/hardware/bytecode interpreter/compiler, mut run correctly. And your proof is not that useful if you did not prove that all these things run correctly too. At the very least, in order to prove your program correct you would need to have some formal specification of the behaviour of the calls you made to the library to USE in your proof. And those things simply do not exist.

Your program is in the end a teensy weensy part of a whole system, unless you are writing some embedded thing on bare metal (or programming a Apple II or C64 or something really simple).

what does this buy me?

[egomaniac]

As a software developer, I'm not sure what this buys me. I can prove that if my software is a 100% correct implementation of the ideal system decribed in Z, then it's bug-free.

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?

Re:what does this buy me?

[Ivan Raikov]

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.

Re:what does this buy me?

[cookd]

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.

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 :)

Re:what does this buy me?

[Alwin Henseler]

"Beware of bugs in the above code; I have only proved it correct, not tried it."
http://www-cs-faculty.stanford.edu/~knuth/faq.html

Re:what does this buy me?

[SEWilco]

you validate that specification against what the user wants

That won't always specify the right program for the application. In one project I was assigned to code a user interface from a nicely detailed specification. When the project team then sent me to test it at the customer site there were many complaints from the users. It was obvious to me that the specification did not match how the users actually did their work.

Apparently some group had designed the user interface to have the computer tell the user what work to do next, but the users actually decided what to do and needed to be able to tell the computer what had been done (although the computer could offer suggestions of what needed to be done).

Re:what does this buy me?

[p3d0]

You can't really think the people working on formal verification are that stupid.

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?

Re:Spell checking?

[pmz]

Z is a formal (i.e., mathematical) specification notation used by industry...

What industry?

In practice, just getting the requirements right is more important. The better the problem domain is understood, the fewer errors--real or percieved--will be present in the implemented system.

Also, I know of no programming language that fully prevents the possibility of side-effects of new code. C allows some pointer arithmetic to totally destroy basically anything in the program. A Java "null pointer exception" can leave disk files or other data in a incomplete state. The best a Lisp environment can do is let the programmer "undo" a problem to try again, which isn't suitable for production code.

So, any change in a program's requirements would require a full re-analysis with this Z and B-method stuff? If this is true, no wonder no one I know ever mentions it.

What I would really want is more and better specifications for data exchange formats, so test suites can be more common for conformance testing and validation. Test suites are a lot of work, but they can become the "living specification" that everyone measures up against (meaning the specifications and test suites have errors but everyone is the same in their wrong-ness).

Re:Spell checking?

[Monkelectric]

side-effects

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.

Re:Spell checking?

[Godeke]

After doing a bit of research on the linked sites, one can see that this falls under the "well meaning and very useful in nitches" category. If you are building software that *can't die* because it will be used in critical points like aircraft control systems or medical equipment, you can probably afford people smart enough to implement this.

The "language" itself looks like a cross between boolean algebra, set theory and relational algebras (which came from set theory). Using a truely functional language would make this much easier to implement (as you point out, procedural languages tend to allow you to wack the state at any time).

So we have a methodology that requires people to understand functional programming and some pretty abstract math concepts to boot. I guess you could have a really well payed designer with those attributes, but most business programmers would be lost forever.

That being said, another comment mentioned Gemplus, a JVM entirely proven by using the B method (which uses the Z language). This is used for smartcards, where "undesired functionality" would mean compromized financials. If it is possible to write a proven JVM, perhaps I fall in the "not bright enough" category to see how.

Re:Spell checking?

[Anonymous Coward]

Ok, this is late and off topic, but your post is freaking stupid. It is not a problem with C; you simply do not do that type of thing.

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

[DancingSword]

So what happens when someone is programming in some language/dev-system that won't permit non-correct program ta be wrotted? Eh?

Also, your determination that grown biological computing is unlikely to ever achieve its ultimate goal, yeah, we prove that, don't we...

: P

( of course, just precisely what our ultimate goal IS be open to debate...
: )

Re:Unit tests seem to be the way to go

[saden1]

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.

Re:Unit tests seem to be the way to go

[Jerf]

So what happens when someone is programming in some language/dev-system that won't permit non-correct program ta be wrotted? Eh?

Ironically, it's provable that no Turing Complete language can be limited to create only correct programs for any non-trivial definition of correctness. Computer science is full of such fun things.

Proof: In your supposed language, there is a set of "correct" programs for some criterion, and a set of incorrect programs.

(Sub-proof: The program "return 1" is only correct for the problem consisting of "Always return true" and isomorphic problems, and "return 0" is only correct for the problem consisting of "Always return false" and isomorphic problems. Thus, for any given correct behavior there exists at least one incorrect program in your language, OR your language contains only a trivial number of programs and as such is hardly deserving to be called a "language".)

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).

By Rice's theorem, no such TM machine can exist. (Indeed, it's fairly trivial to show that any non-trivial definition of "correctness" must certainly include asserting that the program executes in finite time, and therefore a program that could check such a correctness criterion must be able to solve the Halting Problem, if such a machine existed.)

Since any language that only allowed one to express correct concepts is isomorphic to a Turing Machine that correctly validates the existance in that language, and no such TM can exist, no such language can exist, unless it is trivial and the correctness criterion is trivial. In which case as I alluded to earlier, it's hardly worth calling a "language" in the computer science sense.

In fact this sort of proof is one of the reasons I seriously wonder why so many people still seem to be pursuing this. (Fortunately, I see many signs that the field is waking up to this fact and good, dare I say useful research has been starting to get done in the past few years; perhaps the empirical successes of unit testing in software engineering has helped prompt this.)

BTW, no offense but I've been on Slashdot for a while, and I direct this at any replier; if you don't even know what Rice's Theorem is, please don't try to "debunk" this post. Many exceedingly smart people have dedicated their lives to computer science. I only wish I were smart enough to craft these tools, rather then simply use them. Rice's theorum has withstood their attack since 1953 . The odds of a Slashdot yahoo "debunking" this theorem are exceedingly low. (On the other hand, if you do understand what I was saying I of course welcome correction and comment; still, this is a fairly straightforward application of Rice's theorem and I can't see what could possibly go wrong. It's a pretty simple theorem to apply, it's just the proof that's kinda hairy.)

Also, your determination that grown biological computing is unlikely to ever achieve its ultimate goal, yeah, we prove that, don't we...

I do not believe biological computing is impossible; we are an obvious counterexample. What I don't think is going to happen is that at any given point, the most powerful (man-manufactured) computing device that exists is biological, because biological systems by definition require a life support system to support them, which must consume space, power, and resources better spent directly on the actual computation by a non-livi

Re:Unit tests seem to be the way to go

[Anonymous Coward]

It's not about debunking, friend. It's about pointing out that you have Missed The Point.

Any program that correctly does what it was written to do is a correct program. However, not all programs are written to do the right thing.

Formal analysis doesn't help you a bit when you sit down and, very slowly and carefully, write a program that does *exactly* the wrong thing perfectly every time.

(Anybody who's ever tried to dash out a quick multithreaded producer-consumer queueing implementation knows what I mean. You get a couple of things out of order and your queue never drains. Not because your program is incorrect. Because your program is doing precisely what you told it to do, only you told it to do the wrong thing.)

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.

Re:Unit tests seem to be the way to go

[DancingSword]

Right.

( awesome reply, and thank you! )

Firstly, I were thinking of Correct Constructs, and probably this is wholely rong, but my assumption was that a Program is made-up of components, each of which can be proved not-incorrect, so the whole thing feels, to me, fractal... ( perhaps there's blurring between the fractal-type reality and the recursive-type reality in my mind... ), so the components can be proven to be correct-constructs, and the whole can be proven too to be a not-incorrect-construct, NOT assuming that this proves it to be the optimal construct, or even the answer to the correct-question, just its non-broken-ness.., and no I didn't assume that all such checking would be guaranteed to happen within finite time, I was just considering the way the logic felt.

Secondly, our definitions of 'computer' are different: Yours seems to correspond more with 'cognition', mine more with thinking ( cognition all-the-way-through to pattern-gnosis/fuzzy-logic, and including various other things that don't translate into English much.. ). Cognitive-systems probably are more-effectively done in machinery, but didn't Godel prove that self-consistency cannot be identical to Reality?

Also, I'm with (Sir) Martin Rees, where he says that there isn't any obvious upper-limit on Mind, but I disagree with him on one point: in buddhism, it is accepted that once one's got sufficient gnosis/mind evolution, then one can finish-the-job one's self.
Edge 116 : 2003-05-19 : In The Matrix., and hims bio: Martin Rees at Edge.org/3rd Culture

If one's definition of 'computing' is inherently digital/sequential, then the analog-computers used, only a few years ago, do study/model power-grids, would be unable to count-as-valid, even though they used very few parts ( as opposed to millions/billions of transistors+opcodes ), and worked rather well. Our current infatuation with ignoring-analog-processing will hopefully wear-off while we still survive, but it isn't a blindness Universe shares, was my humourous point, is all... We think, and are capable of subtle logic, and are capable of true-perceiving, whereas logic-itself cannot know trueness without stepping outside of its self-consistent-system...

As for the rest you rowte, -sigh- I hope I'll understand all you've referred-to in the next coupla years...

: )

Re:Unit tests seem to be the way to go

[Yrd]

Formal specification helps you avoid that kind of thing in the first place though... if you do your spec right that is! It's still down to the programmer in the end, even an insanely high-level language like Haskell can't protect you from everything (even out-of-bounds errors, you can still try and request element 50 from a 20-element list if you like, and it's not going to like it).

So although they can be very useful, you have to do the spec right in the first place. Which can be easier than getting it right in something like C first, because Z uses pretty much mathematical notation and is thus more ameanable to use in proofs and verification, and also expresses only what you're doing, not how you're doing it, which stuff gets impossibly bogged down with in something like C or Perl or whatever.

Then of course if you have an automatic Z-to-implementation-language generator (I know a B-to-Ada one exists, they used it on some mass transit project in Paris I think and it rocked) you've got a very good chance of the actual functionality of the program working properly, and just need to add the UI etc. That's worth it - just not for every program you ever write.

Re:Unit tests seem to be the way to go

[Jerf]

You are free to believe that the human mind has more power then a Turing Machine. I do too, in the end. (Many do not.)

However, computers are definately Turing Machines, and generally when one discusses "computability", we really are referring to computers, not Mind. Even if in the end the mind really is just a Turning Machine we still do not have the constructs yet to deal with it directly (hence the whole field of Psychology). That's still the domain of philosophy.

I'd also point out that the original context of the question, about the computer language Z, firmly places the discussion in the domain of actual computing ;-)

While analog is different then digital, digital computing can still simulate analog computing to any aarbitrary desired level of accuracy so it's not a fundamentally different kind of computing. (Fortunately, courtesy of quantum mechanics and other noise sources there is a very real limit on how precise analog computers can be, so you do not need arbitrarily detailed simulations; if you'd like a philosophical application of this point, this is often used in support of the serious proposition that we do live in a simulation, since it drastically reduces the amount of computation necessary to correctly simulate our world.)

(If you're thinking of going into serious computer science, make sure you concentrate on what computer science and math means by the word "arbitrary", as in "arbitrarily large"; it's actually the correct way to say what Slashdotters usually use "infinite" (incorrectly) for. A lot of the really philosophically interesting proofs turn on that word.)

Despite some breathless books by over-zealous writers like Penrose, conciousness remains a mystery.

Re:Unit tests seem to be the way to go

[Tom7]

In fact this sort of proof is one of the reasons I seriously wonder why so many people still seem to be pursuing this.

Well, for starters, many systems (I don't know much about Z) don't work this way. They have the programmer write a proof with his code, and that proof system is such that the proofs are easy to validate. What is sacrificed is the ability to write some correct programs in ways that the proof system can't comprehend, but for the most part if you're trying to write clear, maintainable code, you don't want to write the program that way either. (For instance, if you're going to write a little turing machine evaluator in your program to do some of the work, these kinds of systems are going to have a lot of trouble with that.)

Also, just because something is impossible to do in general doesn't mean that it isn't easy or useful to do in specific cases. For instances, using your same argument we know that it is impossible to write programs, in general. (Write the spefication for your program-verifying program, or just write the halting problem down.) But of course we write programs all of the time!

no such language can exist, unless it is trivial and the correctness criterion is trivial.

True, but I think the word "trivial" is pretty misleading here. There are many programming languages with built-in safety properties (SML and Java for instance), where you simply cannot write programs that corrupt memory, execute arbitrary code (ie, through buffer overflows), etc. (Note: this is a property of the language. Java is often compiled to a VM, SML is usually not, but that has nothing to do with their safety properties.) That safety property is "trivial" by your argument, but I think it is a damn useful one.

Unit testing is great for testing the common use-cases of business software. I program in academic safe languages every day, and I still use unit testing. But unit testing can't really catch security holes like buffer overflows (and security misdesigns like protocol errors), and it can't really assure perfect operation in life-critical systems (I know for a fact that BMW uses model checking to verify their drive-by-wire systems work properly). Mathematical proofs are good for catching these corner cases, and though they are probably dozens of years away from being mainstream, I do think they'll get there.

Re:Unit tests seem to be the way to go

[dkf]

But testing isn't enough, especially in a safety-critical area. How do you know that the tests are adequate? How do you know that the tests test what the customer is after? How do you know that the various unit tests imply that the system integration tests will work?

Unit testing is good, but insufficient, and writing a test suite that covers everything to a level that ensures that integration goes smoothly and no faults occur in service is in reality *at least as hard* as using a formal development process, particularly as it is very tricky to work out whether you are testing everything you ought to be testing.

(FWIW, formal software development systems such as Z are enfuriating and bureaucratic, but can really deliver the goods - and with less cost - if you need that level of QA. But word processors don't need quite the same level of quality as railway signalling systems...)

Re:Unit tests seem to be the way to go

[tigersha]

A good example of such a program is any type checker. A specification like the following:

f :: Int -> Char

states that a function in a program takes an integer and returns a character. The Type system should prove this. The thing is, this is in theory impossible by Rice's theorem. Hoever, for a very large (and useful) amount of programs this is quite doable. However, take the following pseudoprogram:

f(x) = if 2 = 3 then return true else return 'a'

This program be rejected by any typechecker even though it does conform to the specification of its type signature. At runtime the program will, indeed, always return a charactrer. This is difficult to see at compiletime by the typechecker hence the checker will reject it since it does not conform to its internal type structural rules (for one, in most type systems both branches of an conditional must return values of the same type)

The set of correct programs that are not caught by the typechecker are called "slack". One place where slack is sometimes a program is a datastructure that contains elements of different types, this is a problem for many typecheckers.

Research into type systems (and there is a LOT of this) tries to extend the type checking algorithms so that slack is minimized while the typechecker proves more and more programs correct, but so that the checker does not become too convoluted. I personally think that the typechecker in some modern functional languages are already going too complicated, but I digress.

However, most typed languages can type almost all useful programs with few problem cases (however exacylt those cases draw the ire of the typeless programming language crowd). THe point is that the heurstic of the algorithms is good enough to cover most of the useful cases without it being universal.

About formal methods

[sl956]

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 :

• J. A. Hall, "Seven myths of formal methods", IEEE Software 7,5 (Sept. 1990), 11-19. ( quoted here)
• J. P. Bowen & M. G. Hinchey, "Seven more myths of formal methods", IEEE Software 12,4 (July 1995), 34-41. ( quoted here)

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).

Re:About formal methods

[MerlynEmrys67]

How about you can fool some of the operating systems some of the time, but you can't fool all of the operating systems all of the time

impossible ?

[wotevah]

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.

ACL2

[Ivan Raikov]

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.

wouldn't a proof imply

[Anonymous Coward]

the theorom was known? Given one of the biggest challenge of software design is functional requirements, how can one form a provable theorom. Let's say I want to write a "Z" proof for quicksort. Sure that's easy enough, since it is very concrete and limited in scope. Now, lets take the case of a word processing program. Let's say for argument sake, the functional requirements define input as normal english words. So proving the word processor is theoritically possible. But in the real world, things don't work that way. Say for example, I run out to lunch and I accidentally drop a book on the keyboard. It holds down a couple keys. The question then becomes, what kind of repeated key behavior constitutes an error and what constitutes intentional action? If I'm writing an novel and I decide to put 100 exclamation marks as a joke, how can the theorom account for that?

Theoroms work great when the number of variables is finite and limited in scope, but when the variables are huge and multi-dimensional, the problem gets very hard. Not impossible, just too time consuming and likely useless. One could write a theorom general enough to test for 95% of all possible permutations, but that could be huge. Having a more directed set of tests in those types of cases is much more efficient than having a program prove your application is bug free based on a theorom. Writing an elegant theorom in a certain extent requires expert knowledge of the problem domain. If that is the case, then it would still be easier to use unit testing as a way to validate the program. Theorom are great in physics and math, but software engineering has too many variables. Most of the most interesting problems are the result of illogical human behavior or unpredictable conditions.

perceived cost v. perceived benefit

[blackcoot]

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"

Re:perceived cost v. perceived benefit

[Tune]

Good point. I'd like to add one.

In my experience - I've worked with a lot of people just coding for the love of it - most coders find specification very hard. The term "Formal Specification" suggests it is a solid way to define program semantics unambiguously. Also, since it is (or should be) a high level language, it should be pretty easy to express complex behaviour.

In reality it is not. Writing a good specification - where good implies not just that it is consistent, but also that it covers the complete problem (and nothing but that problem), it is not too lengthy and is intelligible by people implementing it - is a job unsuited for many, if not most, programmers with average or above average skill. Many of my colleagues with Masters or PhD degrees can't even write proper inline documentation with their code. This is not a matter of learning English but of being able to think abstractly and working very disciplined.

Although I believe specification should always be an integral part of software development, I must say the best and most productive coders are the ones that simply "go out and code". People that know what good code should look like. For a large code base it is far more important to be able to maintain this code than to know that is "correct".

Code Proofs?

[photon317]

Doesn't "proving" the perfection of a body of code mathematically sound like it would basically face the same barriers as encountered in the infamous halting problem? That's not to say it can't be done with sufficient resources for a sufficiently simple body of code, but I would think there would be no general solution that always works in reasonable time for validating real code.

Re:Code Proofs?

[NTDaley]

It's not a matter of chucking the specification at a piece of software and saying 'prove it for me'.

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.

Re:Code Proofs?

[photon317]

Well, yes but you'll notice the very limited data domains of your examples. Programs designed to output a fixed string "Hello World", or count the static range of 1-10, are pretty easy to solve the halting problem on.

What about real input and output though? It becomes quite a task when the user can input (through a keyboard, hardware device, a config file, etc....) essentially unlimited amounts of input data. You can't conceive or test all possible input value permutations in reasonable time, and therefore cannot "prove" the correction operation of the software in all circumstances reasonably.

Re:Code Proofs?

[Anonymous Coward]

You can't conceive or test all possible input value permutations in reasonable time [...]

One doesn't have to do this to prove the correctness of an implementation. What one needs to do is show that all possible input sequences share some convenient common properties, and then use these properties in your proof.

The keyboard and hardware examples you cite are in general reactive systems, for which there are formal specification and proof languages available. TLA+ is an example.

Re:Code Proofs?

[photon317]

When you use these "properties", will you still catch all the bugs you would catch by testing all input sequences though? Perhaps because of a couple small subtle flaws in a few independant peices of your code that are affected by the same input data stream, everything works fine until a config file contains the sequence " ]D[", at which point your code goes into an infinite loop and never comes back. These things do happen (although typical there's something more obvious involved, like terminal bytes and off-by-one errors in lengths or loop iterators).

Re:Code Proofs?

[Anonymous Coward]

When you use these "properties", will you still catch all the bugs you would catch by testing all input sequences though?

You would potentially catch all the errors in the code. They don't call it a proof for nuthin'!

A few things could still go wrong here (which is why I said "potentially"). Maybe you specified the set of possible input sequences incorrectly. Maybe your proof doesn't prove what you think it does. Finally, the proof verifier might itself be buggy.

By the way, it's not possible in general (that is, for all possible programs) to prove that your program doesn't get into an infinite loop, but it is possible to do for large classes of programs. I don't use formal verification tools, but I personally prefer to write loop termination rules that are as simple as possible, so as to minimize the chance of getting into an infinite loop.

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).

Re:What is possible with Z

[mcdrewski42]

So creating a Z specification:
-forces you to be very specific about what correct behaviour is

- Does not take into account changing requirements without rework of the initial model
- Normally cannot factor change into a design in the way that stuff such as design patterns do

Now yes, these are very different issues, but unless you are working on a system that derives some nontrivial benefit from being 'proven' (ie: nuclear, medical etc) then it only has limited scope.

Perhaps the realities of most short-timeframe projects preclude the use of such formal methods in all but a few cases.

Re:What is possible with Z

[pmz]

So creating a Z specification:
-mean more work before coding starts
-forces you to be very specific about what correct behaviour is

Not just more work. Imagine trying to get a customer to agree on a Z specification. They'll probably say, "Z??? Isn't that some sort of science fiction mini-series?". Also, for many customers, not being specific is the only specific thing about them.

This is where the "black art" of programming is most pronounced, because it often has more in common with building architecture or fashion design than mathematics. This is also why most software projects fail to do anything useful and either become figurative dust bunny collectors or "white elephants". It can be quite frustrating.

Re:What is possible with Z

[Anonymous Coward]

- Normally cannot factor change into a design in the way that stuff such as design patterns do

I disagree with this sentiment. My opinion is that design patterns and formal methods nicely complement each other. The modularity obtained by using design patterns means that
- you can make the specifications and proof modular, and thereore simpler, as well, and
- the simplicity of the sub-systems approaches that of the "toys" it is often said that formal methods are only capable of being used with.

The whole point of patterns is to get an implementation that is as simple to understand as possible. Simple to understand == simpler to formalize. In all honesty I have never used formal methods in a production environment, but my philosophy is to write software in such a way that it would be possible to apply formal methods if the need were to arise.

Re:What is possible with Z

[Anonymous Coward]

I came up with one more synergy between patterns and formal methods: modularity increases code re-use, and the more often a module is re-used, the nicer it becomes if it's formally verified.

Re:What is possible with Z

[Anonymous Coward]

"Now yes, these are very different issues, but unless you are working on a system that derives some nontrivial benefit from being 'proven' (ie: nuclear, medical etc) then it only has limited scope."

I suppose "end user" applications like a typing trainer wouldn't benefit much, but lots of things such as operating system kernels, system libraries, mathematical libraries, databases, etc. would seem to gain quite a bit from this. Of course, commercial companies don't have the incentive to go through the work of a Z specification for such things, but perhaps open source could give it a try. Once completed, if the design was good, it might prove to be very very interesting. A stable platform on which to build applications, where behavior was known and proven, might provide a great deal of benefit.

Ask Slashdot?

[NTDaley]

I assume this is supposed to be an 'Ask Slashdot' story.

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

No!

[Tom7]

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.

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: /* terminate and return 1 for any positive input */
int collatz(int i) {
if (i & 1) return collatz (i * 3 + 1);
else return collatz(i >> 1);
} ... 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.

Re:No!

[wotevah]

...hence the vaguely. But I take offense at your "total crap" assertion, especially because after you shot down my statement so categorically, you went ahead to say that actually, it's basically not all that far from the truth...

I should have probably not used the word "impossible" since theoretically it may well be possible, but outside of academia and supercomputing centers, "takes 1 year at 10 TFlops" can be safely equated to "practically impossible".

Re:No!

[Jerf]

No, you're wrong. Please see my post on this topic. It is impossible to prove all programs correct for any useful definition of "correct".

There exist proof systems which you seem to be referring to that function by examining the complete state space of a given algorithm, and validate it against some criteria. This only works on algorithms that have a finite state space. Since Turing Machines are allowed to have arbitrarily long tapes, the state space for some algorithms can also be arbitrarily large, which to put it colloquially would require an infinite amount of time to validate.

This is still useful; communications protocols are useful programs that have a very easily characterizable finite state space, and have been validated to prove there are no deadlocks in them, but that's because communications protocols are typically very simple things with tight loops and a small handful of state variables; they are very much the exception, not the rule, and even these simple, ideal cases for state space examination spin out of control exponentially quickly as more state is added to them.

Ironically, both my undergrad and grad level Software Engineering classes spent a disproportionate amount of time on these system, which are only useful in such a small handful of cases, where our coverage of "testing" consisted mainly of regurgitating the traditional, and damn near useless outside of a classroom, definitions of black- and white-box testing. (Nearly all real testing is some shade or other of "gray"; this grudgingly admitted and immediately glossed over.) Pity the time was spent that way, it would have been much more useful to practice writing tests, not using those state-space provers; there's an art to test-writing and it would be much more useful for just about everybody except someone who is 100% academic. (I'm not; I'm as close to 50-50 as I've ever seen anyone, so I have virtually no use for the state-space provers; elegant in their niche, but I can't help but see it as a very, very small niche.)

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.

Re:No!

[Tom7]

It's not a supercomputing thing, it's just tedious. Verification of a proof is usually really fast. The thing is, it's not "practicall impossible" at all... in fact, it's often very easy. But it is something that has so little benefit over an informal proof that nobody does it for practical software. Sorry if I sounded harsh, but there are a lot of people posting to this story that totally don't understand the mathematics involved or even what they're trying to do, and that drives me nuts. ;)

Re:No!

[Tom7]

Oops, it should return 1 if the input is 1, sorry.

Re:No!

[sweet reason]

/* terminate and return 1 for any positive input */
int collatz (int i) {
if (i == 1) return 1;
if (i & 1) return collatz (i * 3 + 1);
else return collatz(i >> 1);
} ... really, really hard to prove correct.



it had better be hard to prove correct!

called with the most negative integer (high bit set, all others zero) it will return 1.

or did you not mean to specify what it would do with a negative input?

Re:No!

[Tom7]

(?)

The specification is right in the comment before the code. It says that it returns 1 for any positive input.

set theory

[Tablizer]

language called Z, which was based on set theory.

Relational is also based around set theory. I think relational is cool, especially if done right (the current vendors and languages need help IMO).

Relational could also be made more friendly by creating operators and syntax that people can better relate with. The operators can be defined based on combinations of Dr Codd's original operators, but more "natural".

There does not seem to be a lot of pressure to improve upon relational theory beyond the "Oracle model". Chris Date and a few others are about the only researchers making much effort in this field. But they are not very good at marketing their ideas, so most people get confused and ignore them.

I hope that relational gets a "boom" of fresh attention the way that OO did. Of course, some people get carried away during such booms, and create some silly tools or languages.

we're on slashdot, not k5

[llimllib]

adjust your monocle polish jokes accordingly.

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:Requirements drift will kill you

[BobGregg]

Parent should have been modded +5: *Damned* insightful. My friend is working on a tiny little program right now that has been changed completely several separate times within the same week. Formal analysis is *hard*, and takes a long time, even with tools. And once it's complete, a small change to the requirements can break the analysis utterly. With real-world, commercial development, requirements drift isn't just a possibility, it's a near-100% certainly. With the exception of large, safety-related problem domains where the scope of projects is big enough to incorporate time for the formal analysis to take place, using such methods is next-to-impossible. I wish it weren't, but it is.

they're teaching it here...

[ollyg]

I attended Aston University in the UK [ www.cs.aston.ac.uk ] and they are still providing a final year module 'Formal Software Development' based around the Z language.

Perhaps this has something to do with the fact that the final year senior tutor has written a book on it - but that doesn't make it any less (or more) useful.

see:
http://www.cs.aston.ac.uk/phpmodules/displaysyllab usinternet.php?inputmod=CS3120

for the lowdown. So in answer to your question - yes people are still using it, at least academically.

cheers,
olly.

Re:they're teaching it here...

[tobe]

And that final year course probably being the last time I encountered Z before reading this article today...

Should also be noted that Aston (at least when I was there) also thought Ada and Modula-2 to be useful teaching languages.. what marvellously transferrable skills those are...

t o b e

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..

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

[Anonymous Coward]

They still do teach ADA at York, and Z is included in some of the modules taught in the 3rd and 4th years.

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

[Scorchio]

Hmm.. well I know some compsci's that passed through York during the few years after I left got through their degree without touching Ada. Maybe it was made optional, or has been re-introduced since.

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

[Anonymous Coward]

At Aston they /also/ still teach Eiffel, and Ada95 and Java and a whole bunch of other languages - it really suprised me when I left how much they gave me in that short time. I was seriously expecting three years of C/C++.

ollyg (from above post)

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

[hyphz]

> The pseudocode is simple enough, but the Z spec
> took up a whole page.

Who wrote the spec?

If a and b are part of your system state-schema then a swap operation is just:

Swap
delta System
--
theta System adres {a,b} = theta System' adres {a,b}
a' = b
b' = a

Short and not too complex. (The "theta System adres" bit is basically just saying "this operation doesn't change anything other than a and b in the system"; if I knew exactly what your System schema was I wouldn't have even needed to write that. And "adres" means "domain anti-restriction".)

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

[prockcore]

Sheesh, kids today and their poor optimization skills.

a^=b;
b^=a;
a^=b;

Swaps scalars without using an extra variable.

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

[p3d0]

Sheesh, you old-timers and your premature optimization.

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.

That's not the kind of proof I'm talking about

[Tom7]

I'm not wrong. What the original poster said is that it's impossible to prove anything but the simplest algorithms correct. That's not true at all; people publish papers with complicated algorithms and proofs of their correctness every day. Those proofs of correctness can usually be concretized to the source code level, it's just painful. It is not impossible! (There is no limit to finite state spaces. Haven't you ever heard of induction??)

I'm not talking about a computer program that examines raw source code and tells you wether it is correct or not, so your other "proof" doesn't apply. I'm not talking about model checking (that's what you seem to describe above), which can be useful, but not usually for *algorithm* analysis. I'm talking about writing down a proof of correctness, and perhaps checking that proof with a computer.

I happen to think these kinds of methods are not practical today (though they can lead to type systems that are practical). But there is certainly no theorem telling us that it's hopeless.

Re:That's not the kind of proof I'm talking about

[Jerf]

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?

Re:That's not the kind of proof I'm talking about

[Anonymous Coward]

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.

Everything that can be proven is trivial? Tell that to the mathematics community!

Re:That's not the kind of proof I'm talking about

[psmears]

Rice's theorem, roughly speaking, shows that you can't write a compiler that gives a compile error if your program computes square roots, but works fine for all other programs - here the criterion for "correctness" is "doesn't compute the square root of the input data".

However, this doesn't rule out the correctness criterion "contains in its source a predicate calculus proof that it satisfies a property also specified in the source code".

Why not? From a technical point of view, the reason Rice's theorem does not apply here is that our compiler returns different values for programs that have exactly the same behavior (it will allow a square root program that proves it calculates a square root, but not one without such a proof, even though both compile to the same object code) - and therefore the set that it accepts is not the index set of a class of r.e. sets.

More informally, you can argue that this definition of "correctness" is "trivial", in that it can apply to a program that has any behavior: if you have a program that you wanted to run through this compiler, you could insert the specification "either terminates or doesn't" at the start, and it would compile - but wouldn't necessarily do what you wanted it to. However, the compiler is still useful, because if you do provide it with a full valid specification of what you want the program to do, and a proof that the program satisifies that spec, the compiler can check that your proof contains no mistakes.

(Of course this may take quite some effort, and it doesn't prove the specification you entered is the same one your customer wants solved, but that doesn't negate the fact that the compiler is possible!)

into a couple hundred of these things strung together in arbitrary combinations, your proof system necessarily breaks down.

No, that's simply false - for every natural way of combining two programs to make a larger program, there's a corresponding way to join the proofs together... the reason it's hard to apply formal methods to large systems is not that the proof systems break down, but that the programmer's patience does...

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 agree with Tom7, I will read it...

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.

Re:The killer problem with formal correctness

[steve_l]

Good point about market size.

I actually use formal methods when proving that threads syncrhonize/dont deadlock: its a dog to test such things and a bit of mathematics saves a lot of time. The rest of the time: JUnit and CPPUnit tests. The nice thing about tests is that you can automate regression testing -I've never heard of automated regression proofs...

how complicated is Z?

[anthony_dipierro]

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.

Re:how complicated is Z?

[Anonymous Coward]

ph00l!

that's so not what Z is all about. it's about getting the program to do what it's MEANT to, not what you ask it to! by using Z to describe what you want, and then programming that, you avoid any spur of the moment decisions as you code an algorithm, which is typically the source of them nasty bugs.

Problem is usually wrong specs

[Anonymous Coward]

I thought that the most likely cause of software bugs was incorrect specifications. In other words, the code is bug-free and does exactly what you want it to do... but what you want it to do is wrong.

I can't see how a formal system like Z could possibly look past the specification and deduce what you actually intended.

"Real-world" use of Z for software development

[RelentlessWeevilHowl]

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.

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- zxcb.pdf

A Z paper

[bit13]

I finished a class recently that concentrated on using Z for formal modeling. The two professors published a reasonably interesting paper (for Z) on a thread safe X Windows C library binding to the X protocol.

X meets Z: Verifying correctness in the presence of POSIX Threads

Rice's theorem is not relevant to this

[Tom7]

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.

Yes, this is industry best practice

[ENOENT]

It builds. Ship it!

Sample Z source?

[Anonymous Coward]

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

Re:Sample Z source?

[Jon Jacky]

There are some samples of Z on the web at http://staff.washington.edu/~jon/z/z-examples.html

Areas of strength for formal methods

[Chalst]

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.

+1, insightful

[anthony_dipierro]

It's usually quite a few orders of magnitude easier to write correct yet slow code than it is to write correct and optimized code.

Software is still voodoo, that's the problem

[gwisniewski]

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.

Re:Software is still voodoo, that's the problem

[Anonymous Coward]

A coworker in a previous job consistently blamed problems in his software on the platform, the various libraries and the compiler, anything but his own code. When I pointed out an error in his code, he got upset and denied at first that it was an error, then when I explained to him in detail the circumstances in which the error occurred he denied that it was important in any way. He never did fix it.

Meanwhile, we had a 24/7 on-call service for dealing with problems in our product, and about 40 clients. I'm glad I got out of that job.

Answer to question in article title

[Saganaga]

No.

Z is a specification language

[Anonymous Coward]

Z is a way of formally specifying requirements.

When you are developing a system and you are doing analysis of the the system's requirements given, Z allows you to capture a specification of the requirements in a precise manner.

This is the pretty much the bounds of what Z does.

So

It doesn't prevent programming errors.
It doesn't prevent poor analysis.
It does help getting a requirement of a system that is being devloped down in a precise way.
It acts as an abstration of the system(or model of the system).
It is a good reference for a requirement latter on.
And particularly, it allows a requirement to be verified in the early stages of a SDLC, when it is cheaper to change, rather than when it becomes expensive and unwieldly to do so.

I used Z for radiation therapy machine software

[Jon Jacky]

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

No such beast. Provably.

[ZiZ]

Imagine this situation: You have an algorithm which can, given a program as input, determine if that program will function properly. The way to break it is simple. Write a program that performs tasks as the pseudocode following dictates:

Specification: This program will terminate (i.e. finish executing).

Run my own code through the 'properly functions' algorithm
Does it say I'll terminate?
If so, loop forever and never terminate.
Otherwise (it says I'll never terminate) terminate immediately.

It is impossible for the algorithm to return an answer which is correct for this program, and therefore the algorithm itself is flawed.

This is a slight variation of the 'halting' problem. :)

Software Zero Bugs, design one.

[oliverthered]

Ok, so your software will work to the design, but who's going to design perfect software?

Re:No such beast. Provably.

[Anonymous Coward]

If you allow for an "I don't know" reply, then you can write such an algorithm. The problem is then reduced to one of coding practice, i.e. writing code which the automatic verifier is able to verify.

Re:No such beast. Provably.

[p3d0]

Good grief, smart people say some stupid things.

Z doesn't have to prove all programs (including the one you describe) correct in order to be useful. It only has to prove my program correct to be useful to me.

Wrong

[Animats]

The halting problem does not apply in program verification. It's easy enough to produce programs whose correctness is ambiguous, but such programs are broken.

Incidentally, the halting problem is decidable when memory is finite. Either the program halts or it eventually repeats a previous state. This is not enormously useful, because you can write a program with a huge state space, but it answers the formal objection.

Nothing offensive here.

[Anonymous Coward]

No, he did not shoot down your statement that you "vaguely remember that [such-and-such]".

Suppose (1) I vaguely recall that in 1996 Joe proved the halting problem was solvable, and (2)Sue is familiar with the "proof" and knows it to be bogus, and (3) she says "this is crap".

Since I admitted my recollection was vague, she is not likely denigrating my powers of recall. And my admitting my recollection was vague, I am clearly not defending Joe's thesis, but raising it speculatively. I am not actually asserting the thesis, so there is no assertion on my part to denigrate. So what does Sue's "this" refer to? Presumeably the thesis itself.

So I think Tom7 was saying that the "[such-and-such]" was crap. You were not standing by the such-and-such, but essentially saying that you *thought* such-and-such was shown ... right? So the "crap" was in no way directed at you.

At least, this is how I parse it!

relation between formal spec and unit testing

[bramez]

In fact unit testing and formal methods could reinforce each other, but IMO the tools for this approach are missing.

Say the system you want to test has an "input space" (all combinations of possible input parameters) and some output ( a program that doesn't do anything , produce something or has a side effect, is useless). Unit testing is all about defining a series of a "test cases". In each test case we

• set up a precondition;
• deliver an input for the function to perform;
• then do some checks on the result.

Writing a new test case is only usefull when it verifies another "behaviour" of the system. Take a look at the way XP approaches testing:

• write some tests
• then write the code that implements the tests
• then try to "break" the system by writing a test that makes the system fail
• then enhance the code to work with the new test
• retest with all tests to verify regression
• repeat.

If you look at this procedure in a more abstract way you could say that intuitively you are "partitioning" the input space of the method, where in each partition the system has a different behaviour, described by the representative testcase. So a test case is a representative of a whole class of uses of the system where the system has similar behaviour.

A word on my experience with formal methods : When I started writing unit tests, I noticed some similarities with notions of formal methods I encountered at university:

• Hoare calculus also has this structure of pre- and postconditions. Formal verification of programs using Hoare calculus is a bottom-up process: first one specifies a formal proof of a trivial step of a program (e.g. 1 assignment) by describing the state of the program before and after execution of the trivial step (aka describing the pre- and post condition). The verification of such a trivial step consists by simply stating one of the axioms of the calculus. The calculus then provides compositional rules to combine trivial steps in more and more complex algorithms, and in the process the pre- and postconditions of the composed statements are combined in more complex pre- and post conditions for the whole algorithm.

  A similar approach is "stepwise refinement" or "transformation". In this case a method is first entirely formally described, but without an explicit algorithm. The formal description is then step by step transformed into an executable algorithm. Each step is "verifiable", i.e. preserves ths semantics of the formal specification.

• "Abstract datatypes" (ADT's) and "rewrite systems" have notions of "sufficient amount of specification". An ADT is some sort of "mathematical class", where the methods on the class are formally specified by specifying logical statements about relationships between methods.(e.g an ADT "stack" could have methods "push", "pop", "isempty", and a specification "performing a pop after a push on an empty stack returns an empty stack", which is then writtten formally in some logical language like pop(push(isempty())) == isempty(), etc... ) Once one has sated enough relationships between an ADT's methods, it is fully specified. What is interesting is that there are formal methods to tell
  • whether an abstract datatype is "underspecified", so the ADT needs more statements to be fully specified
  • to verify whether a problem is "overspecified".

The similarities are only vague: hoare calculus verifies a method, but the partitioning is oriented on the program structure, not on the input cases. ADT's do not specify a single method, but a whole class, but the similarity is that there is a process of "finding the right amount of specification".

Both formal and unit testing have their own strenghts and weaknesses:

Formal verification

• tends to be very elaborate. a typical comment you hear about formal testing is that it "is only justified for systems where every failure is critical and unacce

Z and Math-Phobic clients

[whistler36]

I looked at Z for a while, but I had a problem with how closely it resembled mathematics. I thought about the momement when I would present a Z specification to a typical client and could not imagine them using it. I would think that they would always go for the text description.
After all, it's the end user who is supposed to approve what you are doing and the typical user is probably someone who avoided algebra in high-school at all costs. Their eyes would glaze over at any mathematics at all. Only the programmers would use it.

Of course I supposed that the text could be could be generated from the Z - but how clean would that look?

'zero defect' development

[aaronli]

Zero defect development is tough to introduce to a development environment because it is so different from what we accept as development. I'm going to make distinctions here between Z, a formal specification, and 'zero defect' development which I believe the author is referring to 'clean room development' Using a formal specification, like Z, a specification can be written for a programming that can be proven to be correct. It's difficult to define 'correct' but essentially the program can be shown not to have any errors of design. With a form specification, the specification of requirments is the design. Following this, formal methods can be iterativley applied to the specification to gradually develop the desired code. At each stage proofs can be offered to show that the code written conforms to the prevous specification + code. When this is done in a clean room environment. The produced code is transfered to a second team who does all the testing. Any fault that is found is considered a fualt of the PROCESS. The code is THROWN AWAY and new code developed from the specification. A recent use of this technique on a large commercial package resulted in just 173 faults being found. ONLY 3 of these were found after release. The biggest problems with these techniques are: 1- Formal specifications are too hard for clients to understand 2- Formal techniques are difficult to learn and use with LOTS of training 3- Throwing away instead of fixing is difficult to comprehend 4- Not all things being developed can be expressed with formal languages. Client Server architectures are very difficult. Especially if they are asynchronous.

Re:'zero defect' development

[oceansoft]

It seems the weak link in this zero-defect cause is the specification. Zero-defect software becomes unattainable without precise specifications.

Zero-defect software should probably be approached from the viewpoint of course-grained systems. Break the problem down into smaller problems and attempt to prove each smaller system is correct. As smaller systems are combined to build bigger systems, the zero-defect approach shifts to proving the integration of smaller systems is correct.

I offer two suggestions for approaching zero-defect software:
- Well-defined API's for each system
- Testing as many permutations of these API's as possible.

The interfaces for each system must be simple for an attempt to prove it's correctness. For example, I once took over an EBPP product's development only to discover 9 API's for paying a bill! Why not just one? Put those 9 API's in the hands of an inexperienced programmer and you have too many chances for incorrect usage. Well defined systems with well defined API's is essential for approaching zero-defect software.

On another project 12 years ago, I had a team of human and automated testers pounding on every reasonable permutation of API usage imaginable, but we still had bugs coming in from the field. We were baffled to say the least, as we could not think of any scenario we did not test. The culprit was our imagination, we did not think many API usage permutations were reasonable, but some of our users did! Testing every permutation was unreasonable for our given project. So how could we test for the dumbest user doing the "dumbest and most unreasonble" things? My answer was to create the dumbest user of all... to build an automated tester which committed random acts. We executed this automated randomized test on a farm of machines over a weekend, and come Monday about half the target applications had produced incorrect results!

The pith of the latter story is testing cannot guarantee a system's correctness, so a stronger emphasis must be placed on defining and integrating software systems. OMG's MDA is a solid approach, as their goal is to integrate and synchronize domain models, system models, and source code models into a single development paradigm. A good system architect can coordinate the demands of both domain experts and programmers to ensure well defined systems and API's. As MDA tools improve, the ability of the system architect to more closely approach zero-defect software also improves.

Randy

Book

[Anonymous Coward]

You can get a book about Z here.

What UML funds, Z creates test suites in Tuxedo...

[Anonymous Coward]

So why write a Z description if you have UML going on and verticalizing nicely? Does it help increase the speed of reading the comprehensive Russel Logic? Are there PalmPilot tools or something? :_)