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

[Andreas Saurwein <saurwein () uniwares com>]

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