From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,a83c46b54bacb7f6 X-Google-Attributes: gid103376,public From: "Pat Rogers" Subject: Re: JOB:Sr. SW Engineers Wanted-Fortune 500 Co Date: 2000/02/01 Message-ID: #1/1 X-Deja-AN: 580495202 References: <3894A823.92EC75D1@bondtechnologies.com> <874b7r$mj9$1@nnrp1.deja.com> <38967537_1@news.jps.net> X-Priority: 3 X-MimeOLE: Produced By Microsoft MimeOLE V5.00.2919.6600 X-Complaints-To: newsabuse@supernews.com Organization: Software Arts & Sciences X-MSMail-Priority: Normal Newsgroups: comp.lang.ada Date: 2000-02-01T00:00:00+00:00 List-Id: "Hyman Rosen" wrote in message news:t73drc6a1k.fsf@calumny.jyacc.com... > "Pat Rogers" writes: > > No. They treated all exceptions as indication of hardware failures > > because they didn't believe > > they could happen due to software. They didn't meaningfully handle the > > exception -- they aborted the program! Since they abused the software > > they were reusing (by using it in a different context, in which > > exceptions were unavoidable) their assumptions were invalid. > > When you have proved that something can not happen, you will not then > add code to handle that event gracefully. After all, that's the entire > point of software proofs in the first place. First, the Ariane 5 people did not prove that exceptions could not happen. The Ariane 4 team did, but Ariane 5 had a different flight profile that made the Ariane 4 proofs invalid for the reused software. You seem to believe that a rigorous, correct proof against something happening means that it cannot happen. I don't agree. For example, all the analysis that says a certain value can never go out of range -- such that an exception handler is not necessary -- is invalidated by the stray particle of radiation that toggles a bit in memory. Just as problematic are the errors in the specifications that the proofs are built against. I am not saying that proofs are inappropriate -- far from it! But ignoring the possibility of errors in proven components is a dangerous approach indeed. > If it turns out that your > proof is in error, it is exceedingly unlikely that the code will fall > back to a reasonable behavior. What's the basis for that assertion? Certainly if there is no design in place to handle errors then there will likely be no graceful response! But that is a (poor) design choice. IMHO one should design the code to respond to the very real possibility of exceptions in a meaningful way. (Ariane 5 did not.) For critical software, that means having a backup if the situation permits. Structured exception handlers are one way of invoking the backup. > Do you see people writing 'if a = 3 and then a = 3' just in case the > first equality was a fluke? No, I see* a certain aerospace company experiencing 4 or 5 errors per year in their flight software. The prove everything rigorously -- the 4 or 5 errors are due to corresponding errors in the specifications. For those cases I hope they have some fall-back approach. *Told to me first-hand by a member of their team. -- Pat Rogers Training and Consulting in: http://www.classwide.com Deadline Schedulability Analysis progers@classwide.com Software Fault Tolerance (281)648-3165 Real-Time/OO Languages