Re: Ada Core Technologies and Ada95 Standards

[dewar@cs.nyu.edu (Robert Dewar)]

iJohn McCabe said

"As I said before, if I can't prove my software meets all of its
requirements, my customer will not accept it."

That sounds reasonable for high-assurance software, but earlier you
talked about using testing as the basis for this proof, which makes
me think that your standard of proof is rather low.

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

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.

Compilers are no different from any other software in this respect,
but certainly the level of proof is not at the level of rigorous
formal proof (we don't even know how to practicaly create a formal
specification of complex languages in the first place -- an EEC
sponsored project to produce a formal definition of Ada 83 resulted
in a couple of large telephone books of fomulae, but still did not
cover the whole language, or form the basis for a practical proof
of correctness of an Ada 83 compiler since it did not tackle some
of the hard parts.