Path: utzoo!attcan!uunet!motcid!skrbec From: skrbec@cell.mot.COM (Brad Skrbec) Newsgroups: comp.software-eng Subject: Re: Some misperceptions about program proof Message-ID: <1751@teal4.UUCP> Date: 20 Mar 90 15:02:09 GMT References: Reply-To: motcid!skrbec@uunet.uu.net Organization: Motorola Inc., Cellular Infrastructure Div., Arlington Heights, IL Lines: 42 hughes@tempest.Berkeley.EDU (Eric Hughes) writes: ><...> >Misperception 1: A program by itself is either correct or incorrect. ><...> I agree that the preconditions and postconditions are what determine whether a program or subroutine is correct or incorrect for the problem domain. However, if the results of a subroutine don't apply to the pre- and postconditions, is the subroutine incorrect, or is it being incorrectly used? If I use a Sine subroutine where I need a Cosine result, the Sine routine isn't incorrect, only inapplicable. >Misperception 2: The proof is developed after the code is written. >This can, of course, be done. The method works best, however, if the >proof is written at the same time as the code. Furthermore, it works >best when the proof guides the construction of the code. It is often >said "a program and its proof"; I have begun to think of "a proof and >its program." The proof development can and often should accompany the development of the code, but it probably shouldn't guide the goal of the code. If the proof contains misconceptions, then they are automatically carried over to the code, and now you have not one source of false information, but two. We use an independent testing group, and they are kept apart from the code designers and writers, so that they have an unbiased view of what the code should do. If the coders start to work too closely with the testers, they tend toward similar false assumptions, and errors go undetected until too late. ><...> >Misperception 3: Writing a compiler which only compiles correct >programs is impossible. This may be a false perception, but I doubt that you'll disprove it any time soon. Again, this all depends on what you consider "correct". Semantically, I think that current technology won't allow this (We have tried AI verification programs that take a week to do what one could do manually in a couple of hours). Syntactically, I believe this is already done by strongly typed compilers such as Ada and some others.