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,59dddae4a1f01e1a X-Google-Attributes: gid103376,public From: Ken Garlington Subject: Re: Software Safety (was: Need help with PowerPC/Ada and realtime tasking) Date: 1996/06/03 Message-ID: <31B2C2F5.1822@lmtas.lmco.com>#1/1 X-Deja-AN: 158248844 references: <31AC0712.29DF@lmtas.lmco.com> <31AD794D.2E62@lmtas.lmco.com> content-type: text/plain; charset=us-ascii organization: Lockheed Martin Tactical Aircraft Systems mime-version: 1.0 newsgroups: comp.lang.ada x-mailer: Mozilla 2.01 (Macintosh; I; 68K) Date: 1996-06-03T00:00:00+00:00 List-Id: Robert A Duff wrote: > > The problem is that, in English, "correct" is an absolute term. If you > say "This flight-control software has been mathematically proven to be > correct", there's a danger that non-programmers will believe, "They've > proven (beyond any doubt) that the software will do what it ought to do" > (i.e. the non-programmer misses the point that "what it ought to do" is > not necessarily the same thing as what the formal spec said). True - which is why, if anyone were to say to me that their software was "proven" to be "correct", I would consider them poor engineers if they didn't also define their terms. (Personally, I don't believe it is possible to "prove" flight control software even matches the spec. It is only possible to reason about the spec mathemetically, and build some level of confidence in its correctness.) > Using the term "correct" as the proof-of-correctness folks like to, > gives a false sense of security, IMHO. *My* meaning for "correct" is > harder to deal with, of course, because it requires human judgement > (what the program *ought* to do, as opposed to what somebody formally > *specified* it should do). Well, that's life. It also means that your definition of "correct" may not be desirable as the basis for releasing flight control software to the field. Usually, we want something more concrete than "it feels right." (Of course, it's perfectly OK for the _developer_ to use an intuitive notion of "correct" as one of the criteria :) -- LMTAS - "Our Brand Means Quality"