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,42427d0d1bf647b1 X-Google-Attributes: gid103376,public From: Ken Garlington Subject: Re: Ada Core Technologies and Ada95 Standards Date: 1996/04/03 Message-ID: <31623F5E.4EAE@lfwc.lockheed.com>#1/1 X-Deja-AN: 145614874 references: <00001a73+00002c20@msn.com> <828038680.5631@assen.demon.co.uk> <828127251.85@assen.demon.co.uk> <315FD5C9.342F@lfwc.lockheed.com> <3160EFBF.BF9@lfwc.lockheed.com> <828475321.18492@assen.demon.co.uk> 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-04-03T00:00:00+00:00 List-Id: Robert Dewar wrote: > > But maybe I am mistaken, are you in fact using formal specifications, > and formal methods to guarantee the correctness of the software, > reasoning at the generated code level (this is normal procedure > for safety critical software). Well, not for DoD software! MIL-STD-882B says nothing about formal reasoning. My reading of DO-178A says it can be used, but doesn't appear to assume it is "normal procedure" by any stretch. Not that I'm saying formal reasoning _shouldn't_ be normal procedure, but I suspect that, at least in the U.S., it's not used to the extent you imply. > Obviously any customer demands proof at some level that the software > meets all the requirements, but the standards of proof vary a lot, > from an essentially informal testing process to a rigorous formal > demonstration of correctness. And I went to the trouble to agree with you that you could not prove the correctness of software. Rats, misled again! :) But seriously, since you appear to accept the use of the phrase "proof at some level" as a reasonable phrase, let's return to what I think was the topic at hand: What should be a reasonable minimum "standard of proof" for the quality of an Ada compiler: a commercial product, but one that is often advertised as suitable for use in building high-integrity software? So far, you've mentioned that: 1. The ACVC is not an adequate standard of proof, because of inherent limitations of a general certification test suite. I'm not sure I fully accept that rationale, but as we've already agreed, you're far more knowledgeable of the ACVC than I, so I'll have to bow to your expertise. 2. The real standard of proof should come from the actions of the individual vendors. In particular, you said that GNAT has a development and test process, and that this process was probably common to other vendors. I requested a description of this process. Is this an unreasonable demand from potential customers like Mr. McCabe and myself? I know that any potential customer can ask for my company's process at any time (in fact, we have booths at conferences like the Software Technology Conference _promoting_ our process).