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: 109fba,baaf5f793d03d420 X-Google-Attributes: gid109fba,public X-Google-Thread: 103376,97188312486d4578 X-Google-Attributes: gid103376,public X-Google-Thread: 1014db,6154de2e240de72a X-Google-Attributes: gid1014db,public X-Google-Thread: 10db24,2243248c6a74be5 X-Google-Attributes: gid10db24,public From: srt@zaphod.csci.unt.edu (Steve Tate) Subject: Re: Should I learn C or Pascal? Date: 1996/07/22 Message-ID: <4t06tj$3a2@hermes.acs.unt.edu>#1/1 X-Deja-AN: 169478665 distribution: world references: <4sord0$l0k@solaria.cc.gatech.edu> <4su04n$fa6@hermes.acs.unt.edu> <4su73k$r68@sunsrv12.clr.com> followup-to: comp.lang.c,comp.lang.c++,comp.lang.ada,comp.edu organization: University of North Texas newsgroups: comp.lang.c,comp.lang.c++,comp.lang.ada,comp.edu Date: 1996-07-22T00:00:00+00:00 List-Id: Robert Dewar (dewar@cs.nyu.edu) wrote: > Steve said > "| poster. To explain that a little better: you can never, EVER "test > | the correctness" of an *algorithm* by executing it. I don't care how > | you design your test cases, the ONLY way to show the correctness of an > | algorithm is with a formal mathematical proof. Of course, > | implementations are good for demonstrating the INcorrectness of some > | algorithms! :-)" > Well it is a reasonable guess that Steve is pretty new to the field and > is repeating what he has been taught. Ummm... no. I've been programming for about 18 years, and have had a Ph.D. and been teaching for about 5. > But still, this concentration on > correctness seems a mistake to me, and it particularly seems a mistake > to concentrate on correctness to the exclusion of pragmatic understanding > of the real issues. > Steve, you need to understand that correctness is just one aspect of a > program. Correct programs are not necessarily usable or acceptable, and > incorrect programs are often both usable and acceptable. There are two > issues here. And you seem to have totally missed what I said. Nowhere (not even once) did I say anything about proving that a *program* was correct. I was talking about correctness proofs for *algorithms*. Take, for example, Prim's algorithm for finding a minimum spanning tree. There are a huge number of different ways you can implement this, using different data structures or different languages, but the abstract sequence of steps that makes it Prim's algorithm is very well defined. Furthermore, you can formally prove the correctness of the algorithm which, of course, doesn't depend in the least on implementation details such as exact data structures of programming language. I think using a real programming language to describe Prim's algorithm would be a mistake because it wouldn't clearly emphasize that these details are not relevant to what "Prim's algorithm" really is. Let me give you another example that better illustrates what I said about an implementation telling you nothing about the correctness of an algorithm. There is a proposed primality testing algorithm (based on a sequence of numbers called the "Perrin Sequence") which was recently (June 1996) described in Scientific American. The algorithm has been known for about 100 years, but noone has been able to either prove that it works correctly or give a counter example. There have been implementations, and for almost a century all empirical tests have shown that the algorithm works. Until a couple of weeks ago. That's when a counter example was found. So I repeat what I said before: you can tell absolutely nothing about the correctness of an algorithm by testing --- the only thing that reasonably shows the correctness of an algorithm is a good mathematical proof. > Correctness only reflects the match between a program and it spec (Note; i > know we had a discussion about the confusion caused by taking a general > term like correctness and using in this restricted sense, but that is clearly > what Steve is talking about when he talks about a mathematic proof, since > clearly you cannot proove a program correct if you use the more general > informal meaning of correct :-) Again, I was talking about algorithms, not writing a program "to spec". When you talk about algorithm, you are normally given a clear, unambiguous, mathematical description of what needs to be computed. Proving correctness is clearly desirable in such a situation. -- Steve Tate --- srt@cs.unt.edu | "As often as a study is cultivated by narrow Dept. of Computer Sciences | minds, they will draw from it narrow University of North Texas | conclusions." -- John Stuart Mill, 1865. Denton, TX 76201 |