Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cornell!oravax!ian From: ian@oravax.UUCP (Ian Sutherland) Newsgroups: comp.software-eng Subject: Re: Have *YOU* ever written a program which COULDN'T be proven correct? Message-ID: <1317@oravax.UUCP> Date: 3 Feb 90 20:23:52 GMT References: <17143@duke.cs.duke.edu> <793@arc.UUCP> <1297@oravax.UUCP> <796@arc.UUCP> <1303@oravax.UUCP> <801@arc.UUCP> Reply-To: ian@oravax.odyssey.UUCP (Ian Sutherland) Organization: Odyssey Research Associates, Ithaca, New York Lines: 111 In article <801@arc.UUCP> steve@arc.UUCP (Steve Savitzky) writes: >In article <1303@oravax.UUCP> ian@oravax.odyssey.UUCP (Ian Sutherland) writes: >>Like I said: the system explicitly assumes that the state space of the >>program is finite. This includes the stack and the heap. It doesn't >>include the file system because the subset of C/UNIX the system handled >>didn't include system calls for accessing the file system. > >I can count the useful programs in this subset on the fingers of one >foot. (Actually, I presume your system handles things like library >routines, so it could have some use, but I couldn't resist. :-) The first version of the system was intended to verify floating point programs of the sort found in the IMSL library of FORTRAN numerical subroutines. There is a large body of people who consider these programs very useful. When I write programs using floating point arithmetic, I try to encapsulate the real numerical computation in subroutines which don't have any I/O. This allows me to change the external interface to the program without having to change the basic numerical algorithms, which are far less likely to need any changes. The ability to verify such routines is therefore very useful. In any case, I/O is being added to the subset, so your comment above will soon be moot. I agree that a verification system which cannot handle I/O is of very limited usefulness. That's why it's being extended. We are also adding things like pipes and forking to the subset. >>The system (which is called Ariel by the way) >>could theoretically derive such bounds, but at present it's probably > ^^^^^^^^ > (almost certainly)---------------------------------------------^ >>not practical to derive explicit bounds except in simple cases. I don't think you know enough about what we're doing to make such a statement Mr. Savitzky. I don't actually think it's as hard to do as I first thought. The thing that's harder is deriving bounds on roundoff error. Stack and heap size should be easier. At any rate, figuring out bounds on stack size was not a real high priority for the Ariel project because the kinds of routine we were trying to be able to verify almost never nest function calls to a depth of more than, say, 3. Many of them are sufficiently small that they don't call any other functions at all. When we get to the point where we're working on programs which are sufficiently large that this might be a problem, we'll worry about addressing that problem. The analogous comments hold for heap size. >>What >>we do instead is to prove that the program will run correctly (whatever >>that means for a particular program) on a sufficiently large finite > ^^^^^^^^^^^^^^^^^^^^^^^^^ >>machine. ^ > ^^^^^^^ |______ > | >Good! Whether or not you know it, you're agreeing with me. + What you don't seem to realize Mr. Savitzky is that I've been agreeing with most of what you've been saying all along. >I can, for example, write a Turing Machine simulator, and you can >prove that it works correctly unless it runs out of memory. This is NOT what we prove. Lots of systems can prove that a program will work correctly if it does not run out of memory. What we prove is that the program will work correctly if it does not run out of memory, AND that there is SOME amount of memory which is sufficient. As I said in my previous posting, this rules out programs that could use unbounded amounts of stack or heap. Perhaps you don't think that catching bugs of that sort is important. I do. >But you >CAN'T determine (in a reasonable amount of time) under what >circumstances it will run out of memory (because the Busy Beaver >function grows faster than any computable function)! This comment reminds me of the comments in other newsgroups about verification and the halting problem. I don't have to be able to figure out how much memory ANY program will use in order to have a useful system. I just need to be able to prove something useful about useful programs. In fact, I don't need to be able to figure out ANYTHING about stack size OR heap size OR disk usage in order to have a USEFUL system. There are huge numbers of bugs in programs that have nothing to do resource exhaustion. If a system addresses these bugs then it can be useful. Of course, I'm not trying to make this argument for our system because we DO intend to address such problems. >Unfortunately, unless you *can* derive explicit bounds, you can't >prove that your program isn't correct but such a memory hog as to be >useless on anything but a toy problem. You are quite right, but as I said above, a system does not need to address all kinds of bug in order to be useful, and as I said in my previous posting, we're working on it. [my explanation that Ariel will catch unbounded stack and heap usage deleted] >Again, you're proving MY point, which is simply that verification has >certain limits which are often forgotten, brushed aside, or blythely >ignored. (I further argue that IT IS DANGEROUS TO IGNORE THESE >LIMITS.) Again, I already agree with this. If this is your major point, then (a) I think you've made it adequately, and (b) I don't think anyone's arguing with you. I'm certain that I'm not, so stop arguing with ME, OK? -- Ian Sutherland ian%oravax.uucp@cu-arpa.cs.cornell.edu Sans Peur