Re: Ada Core Technologies and Ada95 Standards

[Ken Garlington <garlingtonke@lfwc.lockheed.com>]

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).