Proving Software Correctness

[CajunCenturion]

Can you prove that some piece of software has no bugs?
Edsger Dijkstra said no when he said

Program testing can be used to show the presence of bugs, but never to show their absence!

I believe that the statement is true. You cannot never prove there are no [more] bugs in any given piece of software. You can only say there are no more known bugs.

On the other hand, thargtheslayer posted

Actually I differ with the illustrious Mr Dijkstra on that one. It demonstrably is possible to prove that software is working correctly, by the use of automated unit test tools and the like.

For example, I believe that the 4 colour map problem was solved several years ago by computer. The protagonists (I believe) simply set a computer to explore every possible combination of maps and awaited the outcome. Obviously this must have relied upon some form of topology, but I am not mathematically competent to pass judgement.

So, if a program has a domain space of say 10 billion outcomes, one can set a test tool running to explore its performance under each and every circumstance which may ever arise. By such exhaustive examination, it is therefore (in my opinion) possible to prove that a program has no bugs within a restricted solution domain.

I believe that Mr. Dijkstra was speaking in general, and his statement is therefore self-evidently true, but I assert that it may be possible to demonstrate to the contrary in restricted answer domain problems.

thargtheslayer has made some good point, but raises a number of questions.
[li]Does "prove that software is working correctly" mean the same as "prove the absence of bugs"?[/li]
[li]Can you prove that a program has a fixed domain space of outcomes when initial data condition are variable? User input is involved?[/li]

If you use an automated test tool, it would be necessary to prove that every possible path through the program is tested with every possible set of initial condition with every possible data input option along the way. How can you be sure that there is not another path with a different data set that leads to a failure?

With respect to the assertion that "it may be possible to demonstrate to the contrary in restricted answer domain problems", I believe the validity of the assertion is directly proportional to the amount of restriction is the answer domain. And that's if you can prove a restricted answer domain, and of course, whether that restriction is reasonable within the problem space.

For everyone, please share you thoughts.

--------------
Good Luck
To get the most from your Tek-Tips experience, please read
FAQ181-2886
As a circle of light increases so does the circumference of darkness around it. - Albert Einstein

 

[CajunCenturion]

thargtheslayer - Absolutely. There is a class of programs with infinite space where a proof by induction could work. Unfortunately, I don't think it will work in all cases.

==>I would say that the 'something' is a matter of the validation time becoming unrealistic.
stackdump - In some classes of programs that is correct; it's simply that we don't have the processing power nor the time. But in those cases, it IS provable. There are a finite number of grains of sand and even though we can't count them, we know it's a finite number. On the flip side, it doesn't matter how much time and processing power you have, you can't count the number of states in an infinite state process. In this case, the 'something' is not a lack of time or power, it's having to count to infinity.

Great discussion guys.




--------------
Good Luck
To get the most from your Tek-Tips experience, please read
FAQ181-2886
As a circle of light increases so does the circumference of darkness around it. - Albert Einstein

 

[flapeyre]

It's quite simple, IMO.
You cannot prove software is bug-free simply because you cannot prove that the testing methodologies are bug-free, either.

As it happens, I am working with a web-based automated testing tool to test a new version of an application we have. This tool is, IMO, as buggy as an ant farm. There is no such thing as a bug-free testing tool, since they themselves are written by humans.

-- Francis
I'd like to change the world, but I can't find the source code.

 

[lionelhill]

As a technical user, it's really nice to see a group of programmers discussing whether you can check your software is bug free.

I had an illuminating fight with a large manufacturer of laboratory instrumentation (who shall remain nameless).

The start-point was clear: If I clicked on a certain menu item, it produced results that were mislabelled, so the data were not what they said they were. Production of faulty data is, in my view, a serious bug. The instruments concerned are used by labs (though not mine) to produce evidence that has to stand up in court, so we're not wibbling around with trivia here.

It took me months to persuade them there was a problem. A major hurdle was the local company rep (since moved on), who wouldn't ask the programmers if it was a bug, because he didn't want to bother them (he only felt he could ask them a fixed number of questions per month, and he'd reached his quota).

When he finally did, the response was roughly this: "Yes, this is a bug. No, we're not going to fix it. If you were likely to be misled by it, we would, of course, fix it, but since you know it exists, you are not going to be misled, so we won't fix it as we have other priorities".

So a bug noone knows about is a priority, but as soon as we know a bug exists, it stops being a priority because it's known???? Strewth!

 

[stackdump]

Lionel, nice story, I really like that one. I was told about someone that was code reading an app and got to a line where the code ran dry. The comment above it read "if the user has got to this point, they're screwed anyway, so break".

 

[lionelhill]

like that one too! But as a user, just do make sure it doesn't pop up a window saying "You're stuffed". We prefer the less abusive and more conventional:

"XFG66Te.dll has encountered a proton torpedo at $00000012:FF451203 and is terminating with error code 0d13222768. All your data will be lost and your system trashed, probably for ever. Please contact your local taxidermist and quote your 265-digit license number if this reoccurrs" with a little button saying "Ok".

Oh, and can we please have a button for "not OK"??