RE: Bug-free software (was: Re rant about viruses on VMS...)

["David Crocker" <dcrocker () eschertech com>]

Andreas Saurwein wrote:

> >
With the guarantee that both the B->ADA compiler and the ADA compiler are
bugfree, right?
Also of course granted that the embedded hardware and its BIOS is bugfree.

I have worked myself on "embedded hardware" where the processor itself did
not work as specified by the producer. How do you make a program bugfree
under this conditions? Anybody remember the pentium bug?

Sorry, but I do not believe that anybody can claim to have any piece of
non-trivial bugfree software.
<<

There can of course be no absolute guarantee that any kind of system is
completely free from defects. Nobody can guarantee that the bridge I will drive
over tomorrow won't collapse due to some unknown defect. But for practical
purposes, I can assume that it won't (barring earthquakes and tidal waves).

Similarly, it is possible to build software that is, for practical purposes, bug
free (rather than building software that is almost certain to contain bugs as is
usually the case).

Perhaps you are not aware that since the Pentium bug, both Intel and AMD
engineers have employed mathematical methods to prove that their floating-point
units function correctly for all inputs. My information is that Intel uses
model-checking, while AMD uses theorem proving.

In any case, it is very rate that hardware fails to perform according the
specification that software producers code to. Apart from the Pentium FDIV bug,
can you name any other comparable problem with x86 processors that had similar
ramifications? Personally, I would be delighted if all the software I use was as
reliable as the hardware it runs on.

Similar considerations apply to compilers. Instances of compilers producing
object code that is not semantically consistent with the source code, while by
no means unknown, are actually quite rate in mature, mainstream compilers. If
the compilers themselves were built using the sorts of technology I advocate,
code-generation errors would be virtually unknown.

The vast majority of bugs are not caused by faulty compilers or faulty
processors, they are caused by use of outdated methods of program construction.
Using better methods of software construction together with mature compilers and
mainstream hardware, while one can never totally guarantee that the end-product
is bug-free, one can produce software that is, for practical purposes, bug-free
in the sense that it can be depended on.

By "bug free software" I mean software that behaves entirely in accordance with
the original defined requirements. Getting the requirements right is another
matter altogether.

David Crocker
Escher Technologies Ltd.
www.eschertech.com
Tel. +44(0)1252 336565  Fax +44(0)1252 320954


-----Original Message-----
From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED]
Behalf Of Andreas Saurwein
Sent: 05 February 2004 16:31
To: David Crocker; [EMAIL PROTECTED]
Subject: RE: [SC-L] Bug-free software (was: Re rant about virii on
VMS...)


At 5/2/2004 06:43 Thursday, you wrote:
> No, there are some nontrivial pieces of software in which bugs have never been
> found and there is no reason to believe any exist. I'm thinking here of
> safety-critical software developed using formal specification, verified
> refinement and automatic code generation, such as the METEOR system that
> controls driverless trains on the Paris metro. To quote from the paper by
> Patrick Cousot and Radhia Cousot:
>
> "The 115 000 lines specification written in B compiles into a 87 000 lines ADA
> program. ... Since the metro is running, no error was ever claimed to be found
> in the embedded software nor in its B specification.

With the guarantee that both the B->ADA compiler and the ADA compiler are
bugfree, right?
Also of course granted that the embedded hardware and its BIOS is bugfree.

I have worked myself on "embedded hardware" where the processor itself did
not work as specified by the producer. How do you make a program bugfree
under this conditions? Anybody remember the pentium bug?

Sorry, but I do not believe that anybody can claim to have any piece of
non-trivial bugfree software.

Andreas