Re: "Tracking the Blackout bug"

["Robert I. Eachus" <rieachus@comcast.net>]

Peter Amey wrote:

> The developers did NOT do everything they could.  They could have used 
> the Ravenscar profile in Ada; they could use RavenSPARK; they could have 
> done some model checking of the concurrent parts of the program.  They 
> did NOT test exhaustively because it is impossible (/exhaustingly/ I am 
> willing to believe).  And software doesn't HAVE to be cr*p!

I totally agree, using Ada to write the software would not have 
prevented the problem, it just would have made it obvious.  (Hmmm.  How 
do we handle an exception in the alert system?)  Using SPARK of course, 
would have prevented the problem.  (If you can't prove it doesn't raise 
exceptions or have race conditions, it isn't SPARK.)

-- 

                                           Robert I. Eachus

"The terrorist enemy holds no territory, defends no population, is 
unconstrained by rules of warfare, and respects no law of morality. Such 
an enemy cannot be deterred, contained, appeased or negotiated with. It 
can only be destroyed--and that, ladies and gentlemen, is the business 
at hand."  -- Dick Cheney