Bug Free Software

Some software is used as a component in life-support systems -- meaning that if the software does the WrongThing people will die.

For example, some of the software used in commercial airplanes, the Nasa SpaceShuttle, automobile AntiLockBrakes?, and possibly microwave ovens.

and medical devices - see WillyWonkaConflictResolution

What techniques are useful when writing life-support software? Perhaps they would be useful even in non-critical software -- since "it takes less time to do it right than to do it over".

What techniques are not useful when writing life-support software, even though they're good (or at least common) in writing non-critical software?

What techniques are useful for convincing yourself and others that a piece of software is bug-free? (For example, how do you convince the Appropriate People that a gleaming new airplane with freshly-written avionics software is "safe enough"?)

Is it even possible to write bug-free software? Yes.

(EditHint: does this section say anything new that E. W. Dijkstra didn't say better back in his 1969 paper "Structured Programming"?)

I think Knuth distinguishes between BugFreeSoftware, which is one of those things Goedel proved you can't prove, and PerfectableSoftware.

How did Goedel prove you can't prove BugFreeSoftware?. You do realize that it is actually possible to prove software correct? (i.e. bug-free)? See CoqProofAssistant for more details.

First, I think he was using KurtGoedel as an analogy. Goedel talked about the provability and incompleteness of math, etc... However, I would think regardless of what CoqProofAssistant does, it doesn't prove software is bug free. This is an impossibility. There are an infinite number of configurations, environments, and so on and it is impossible to test in each one of them. That doesn't mean you shouldn't attempt to create BugFreeSoftware, it's just impossible to prove. Go beyond even these factors and you have to start factoring in bugs in the languages and tools you use. Software will never be "provable" until it is quantifiable. You can't quantify software until you can give 10 software engineers the same exact specification, give them the same language to use, and have them independently create the same source code. See IsComputerScience and BugFreeDoesntSell. -- RobertDiFalco

I have absolutely no idea why "have them independently create the same source code" is an issue here. It's possible, in theory, to verify mathematical proofs (if they're written out in mind-numbing detail) mechanically. That doesn't mean that if you give 10 expert mathematicians the same statement and ask them to prove it they'll all give identical proofs. So what? -- GarethMcCaughan

The configuration and environment the program is in is part of the "software." Also, if you can show that all the configurations and environments are correct and so is the program, then you can use mathematical induction to show the software is correct provided the configurations, environments and programs' correctness aren't dependent on each other. (i.e. your code doesn't attempt to rewrite the OS in place) -- SunirShah, admittedly pushing the argument a little hard

There is a hardness to math that does not exist in software programming. Programming is nowhere near as expressive or precise as most models of mathematics. A mathematical model seems such a different thing than a software program I couldn't even begin to compare them. Gödel demonstrated that within any given branch of mathematics, there would always be some propositions that couldn't be proven either true or false using the rules and axioms ... of that mathematical branch itself. If that is true for math, how can you believe that some program is going to be able to prove any of the current batch of piece-meal programming languages? Now, this doesn't mean one shouldn't strive for perfection. Quite the contrary, we just shouldn't rely on some tool that claims to mathematically prove the correctness of software. I'd run from that like it was wildfire in a dry forest. I'll stick with my UnitTesting for now. -- RobertDiFalco

See ProofsCantProveTheAbsenceOfBugs

No-one is claiming to have software that can examine any program and say whether or not it is bug-free. Goedel certainly rules that out. Goedel doesn't rule out the possibility of writing a program and proving that it's correct - i.e., that subject to certain assumptions, carefully spelled out, it will give the right answers. Those assumptions include things like "the compiler isn't broken" and "the hardware won't fail".

It's perfectly true that at present we only know how to do this in very easy cases. It's possible that it will never be practical to write real software this way. But this has nothing to do with statements like "our program languages are unquantifiable", and nothing to do with Goedel. The methods of pure mathematics are often much less useful than more empirical techniques, but they still have their place. -- GarethMcCaughan

Turing is more relevant here than Goedel. See HaltingProblem.

There is no such thing as bugless software.

I see this repeated almost endlessly. It seems to be a case of "I can't write bugless software therefore no one can." Can you not even write a bugless "Hello World" program?

Probably not (that is, probably no one can). If you look at the GNU "hello world" distribution, for instance, it had a glaring bug for something like a decade, yet thousands of people said nothing. Therefore even claims that trivial programs have been bug-free are suspect.

Let's play "hunt the bug". Here's a program in C that is intended to return 0: 

    int main(void) { return 0; }
Can you tell me where the bug is?

You got me. That appears to be bug free. In implementation, anyway; naturally doubts remain about its suitability to address the business policy it was theoretically designed to address. :-)

OK, we're agreed then that it's possible to create a bug free program. Questions remain such as whether the specification is correct, the compiler is correct, the processor is correct, and that no cosmic rays flip bits in the machine while it runs, but at least we have agreed that there is at least one program that is bug free. Yes?

What is a bug?

What a perfect question. My definition: A bug is unexpected behavior. Thus, some bugs cannot be verified formally because they are semantic. Logic errors can, but they are only a subset of bugs. -- SunirShah

How about this:

One implication of this is that you have to distinguish between correct and free of bugs. By 'correct' I mean: the program does exactly what the specification requires, no matter if the specification is perfect or stupid. By free of bugs I mean: the program will, as long as there is no failure in the hardware or another system it relies on (e.g. OS), never do anything the users/architects/PointyHairedBosses who made the specifications would consider a bug. There are indeed well researched methods for proving correctness, but I never heard of any method that could prove that the program will never be very frustrating for its users. And by very frustrated I mean, in the case of 'mission critical' systems, very dead.

Doesn't Xp address this issue directly?

First up, let's not talk about "bugs", lets talk about "defects". Bugs are who knows what, and they appear as if by magic. Defects are pieces of code that cause undesired behavior when executed. They are the result of a developer making an error. The developer made a mistake and wrote some code that does the wrong thing.

Where does proof enter into this? Nowhere, I contend. So we can't prove that a given chunk of code has no defects. So what? We can prevent any defects manifesting as errors, however.

Suppose that we have a body of code with a suite of functional tests that reflect a number of user stories. All the functional tests pass. How then can there be any defects in the code? The users may want to change the stories, of course, having seen via the running system what they really mean. Fine, so change them. Once again, no defects.

So the users using the system within it scope observe no undesired behavior, and all the desired behavior. Great: no defects!. There may be infelicities in the code, so refactor it, that's your problem. It may not perform sensibly when people attempt to use it outside the scope defined by the user stories, but that's their problem.

Hardware doesn't enter into it much either. If my word-processing session doesn't survive a hardware failure, that probably isn't a defect. If my ATC system doesn't survive a hardware failure, well that probably is, but there better be a user story somewhere that says to what extent functionality must be preserved under what failure mode. If that story is satisfied, then there are no defects.

I'd contend that any software that, at some time, performs correctly (as determined by the users) when used within its scope (as defined by the users) has no defects at that time. -- KeithBraithwaite

If you really want BugFreeSoftware, or the closest thing humans have been able to get to it without formal proofs (which tend to be uneconomically expensive, and yet still fallible), see CleanroomSoftwareEngineering

You can prove that the program conforms to the requirements. But can you prove that the requirements correctly specify what the user really wants?

See: http://www.despair.com/demotivators/med24x30prin.html

...for the "motivational" ;-> message: "MEDIOCRITY -- It takes a lot less time, and most people won't notice the difference until it's too late."

A few quotes from "Structured Programming" by Edsger W. Dijkstra (1969) published in the book Classics in Software Engineering edited by Edward Nash Yourdon 1979 [http://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/EWD268.html]:

If a large program is a composition of N "program components", the confidence level of the individual components must be exceptionally high if N is very large. If the individual components can be made with the probability "p" of being correct, the probability that the whole program functions properly will not exceed 

  P = p^N.
For large N, p must be practically equal to one if P is to differ significantly from zero.

...

An assertion of program correctness is an assertion about the net effects of the computations that may be evoked by this program.

...

Program testing can be used to show the presence of bugs, but never to show their absence! Therefore, proof of program correctness should depend only upon the program text.

...

program correctness can be proved [but] the amount of labor involved in proving might well (will) explode with program size.

Therefore, I have not focused my attention on the question "how do we prove the correctness of a given program?" but on the questions "for what program structures can we give correctness proofs without undue labor, even if the programs get large?" and, as a sequel, "how do we make, for a given task, such a well-structured program?" ...

This ... "constructive approach to the problem of program correctness," ... in a number of specific, very difficult programming tasks I have finally succeeded in constructing a program by analyzing how a proof could be given that a class of computations would satisfy certain requirements; from the requirements of the proof the program followed.

...

What is a bug?

I define a bug as anything that prevents a user from doing his job. This includes both misimplemented code and missing features. Believe me, the user really doesn't care why the software prevents him from doing his job.

Can you write some sort of formal proof to handle this definition of a software bug? No, but we still need to develop the software. The problem is not how to prove BugFreeSoftware, but how to develop BugFreeSoftware.

-- WayneMack

So, if the user becomes confused or changes their mind about what they want to do, it's a bug in the software? Say, office politics or the business environment changes, and the old software doesn't happen to match the new environment; that too is a bug in the software?

I would expect to receive a bug report in this case. I believe the user would feel it is a bug is the software is confusing or did something other than what he expected. The software may do exactly what the programmer expected, but the software is not written for the programmer. As long as we are concerned with assigning blame for a problem rather than trying to ensure correct operation, we will continue to have arguments over "bugs" and what a "bug" is. The end result is still the same, either the software adapts to the user or the user adapts to the software, and this decision needs to be made, not on the basis of who is at fault, but on the basis of cost effectiveness and priority.

"They Write the Right Stuff" article by Charles Fishman 1996 about the software programmers who write the software for the space shuttle. http://www.fastcompany.com/online/06/writestuff.html "The way the process works, it not only finds errors in the software. The process finds errors in the process."

see: StaticTypingRepelsElephants, WhatsWrongWithThisCode, BeWrongVisibly, ProofCarryingCode

Perhaps ProgrammingRequiresPerfection is related. DoesSoftwareQualityMeanNoBugs, WhenDoYouCheckForBadArguments, CategoryQuality, DoingUmlForRealTimeSafetyCriticalSystems WillyWonkaConflictResolution RealTime EmbeddedExtremeProgramming FaultTolerance IsYourCodeThatImportant

VotingMachineDiscussion - voting machine bugs don't directly cause anyone to die ("violate their right to life"), but they violate other rights that many people think are just as important ("Give me liberty or give me death" -- Patrick Henry).

(perhaps BugFreeSoftware should be renamed to indicate what we are talking about - WritingCorrectSoftware? or CodeThatJustWorks? - rather than a negative description).

Bits of LifeCriticalSystems should be moved here to BugFreeSoftware, and some bits here should be moved there ... Or should we just combine the 2 pages into one big happy page?

CategoryRealTime

EditText of this page (last edited January 2, 2010) or FindPage with title or text search