steve@hubcap.clemson.edu (Steve Stevenson-Moderator) (01/09/90)
I'm trying to discover the real reason why people do not prove their programs are correct. I would like to collect those reasons --- even those snappy one liners that we all use as excuses. Please forward your comments ( short flames ok) to me by E-mail. I'll post the replies if there is sufficient interest. Thanks. Steve (really "D. E.") Stevenson steve@hubcap.clemson.edu Department of Computer Science, (803)656-5880.mabell Clemson University, Clemson, SC 29634-1906
cooper@nunki.crd.ge.com (Clark Cooper) (01/17/90)
You can prove your program correct with respect to a formal specification, but not with respect to an ill-defined and fuzzy world with which the desired system must deal. The source of most profound bugs is a conceptual model that fails to fit the real world. Proving a program correct with respect to a specification with a faulty model is not only wasted effort, but leads to a very false sense of security. In my view, specification writing is just programming at a higher level. If the language of the specification is truly formal and complete, then (in theory) no further programming is necessary and a suitable compiler could deliver the program. In that case, proving the program correct is like proving that my current compiler transforms my source program into an equivalent program in machine language. The people who worked on the compiler should take reasonable measures to assure that this happens for all valid source programs (and that invalid source programs raise exceptions). If a proof is possible and reasonable for this, then it is a GOOD THING. In any case, it is not the duty of every programmer that uses the compiler. Thus, unless the application domain is purely formal (like program compilation), program correctness proofs are no more than additional evidence that our systems are reliable. This makes them no more valuable than program testing techniques, which are anathema to the program correctness proof school. -- =================================================================== Clark Cooper GE Corporate R&D cooper@nunki.crd.ge.com (518) 387-5887 P.O. Box 8 / K-1 4C31 coopercc@crdgw1.ge.com Schenectady, NY 12301 ...!uunet!crdgw1!coopercc