Path: utzoo!attcan!uunet!samsung!brutus.cs.uiuc.edu!apple!arc!steve From: steve@arc.UUCP (Steve Savitzky) Newsgroups: comp.software-eng Subject: Re: Have *YOU* ever written a program which COULDN'T be proven correct? Message-ID: <801@arc.UUCP> Date: 1 Feb 90 18:46:06 GMT References: <17143@duke.cs.duke.edu> <793@arc.UUCP> <1297@oravax.UUCP> <796@arc.UUCP> <1303@oravax.UUCP> Sender: news@arc.UUCP Organization: Advansoft Research Corp, Santa Clara, CA Lines: 76 In article <1303@oravax.UUCP> ian@oravax.odyssey.UUCP (Ian Sutherland) writes: >In article <796@arc.UUCP> oravax!cornell!uw-beaver!rice!cs.utexas.edu!samsung!brutus.cs.uiuc.edu!apple!arc!steve steve@arc.UUCP (Steve Savitzky) writes: >>In article <1297@oravax.UUCP> ian@oravax.odyssey.UUCP (Ian Sutherland) writes: >>>I managed a project to build a verification system for C programs >>>which use floating point arithmetic. This system makes the explicit >>>assumption that the state space of the program is finite. I like to >>>think our proof methods are getting to the practical stage :-) >> >>What about the stack, the heap, and the file system? > >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. :-) >>Could you >>actually derive bounds on, say, the disk usage of a program? >Since we didn't have the file system included in the state, the answer >is of course "no", but as for the stack and the heap, the answer is a >little more subtle. 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. 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. + I can, for example, write a Turing Machine simulator, and you can prove that it works correctly unless it runs out of memory. 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)! 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. > This kind of analysis will detect problems like unbounded >recursion or unbounded use of space on the heap. For real arithmetic, >we essentially prove that any desired degree of accuracy in the result >could be achieved by running the program on a machine with sufficiently >accurate primitive real arithmetic operations (+, *, etc.). Of course, >explicit numerical data would be nicer, but is harder to come by. >We're working on it ... 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.) My thinking on this subject has been influenced by my very first programming assignment, 25 years ago or thereabouts. Someone had written a polynomial equation-solver that worked perfectly on some very nasty, ill-conditioned test cases, but gave hopelessly incorrect answers on any practical problem. You can guess why: it operated by repeatedly transforming the polynomial to square the roots (ten times), and any reasonable coefficients would overflow. I fixed it by writing a very-extended-precision floating-point package. If it had gone through the fortran equivalent of your verifier it would have passed, bug intact. -- \ Steve Savitzky \ ADVANsoft Research Corp \ REAL hackers use an AXE! \ steve@arc.UUCP \ 4301 Great America Pkwy \ #include \ arc!steve@apple.COM \ Santa Clara, CA 95954 \ 408-727-3357 \__________________________________________________________________________