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: dewar@cs.nyu.edu (Robert Dewar) Subject: Re: Ada Core Technologies and Ada95 Standards Date: 1996/04/02 Message-ID: #1/1 X-Deja-AN: 145521890 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> organization: Courant Institute of Mathematical Sciences newsgroups: comp.lang.ada Date: 1996-04-02T00:00:00+00:00 List-Id: 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.