Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cs.utexas.edu!uwm.edu!rpi!brutus.cs.uiuc.edu!apple!rutgers!mcnc!duke!romeo!crm From: crm@romeo.cs.duke.edu (Charlie Martin) Newsgroups: comp.software-eng Subject: Re: Have *YOU* ever written a program which COULDN'T be proven correct? Message-ID: <17229@duke.cs.duke.edu> Date: 1 Feb 90 14:41:33 GMT References: <7598@hubcap.clemson.edu> <9630012@hpirs.HP.COM> <17080@duke.cs.duke.edu> <789@arc.UUCP> <17143@duke.cs.duke.edu> <793@arc.UUCP> Sender: news@duke.cs.duke.edu Reply-To: crm@romeo.UUCP (Charlie Martin) Organization: Duke University CS Dept.; Durham, NC Lines: 103 In article <793@arc.UUCP> steve@arc.UUCP (Steve Savitzky) writes: >>>Actually, all that is needed is for a machine to have *infinitely >>>expandable* memory, and mine has that -- I can always go out and buy >>>another disk. (One of my professors once described a Turing Machine >>>as having a tape that ran out the door and into a paper factory.) >>You will always always always run into a limit: the number of slots for >>disk controllers, the number of disks per controller, the addressing >>capability of the bus, something. > >I was referring to diskettes, not drives -- I never said that manual >intervention by an operator might not required. Yes, you will run >into limits (including the heat death of the universe); the point is >that a computer can be treated as a Turing machine FOR ALL PRACTICAL >PURPOSES, (Oops; I forgot -- verification isn't practical! :-), >because you can't put a finite upper bound on its number of states. > Weren't we carrying on this argument by mail just a day or two ago? Or was it someone else? In any case, you won't see ME asserting that verification isn't practical. I regularly write programs with proofs. I regularly code them in C. I regularly write programs which have zero defects during testing and zero defects in the field in real use. I'm talking about multiple-thousand line programs doing hard system-programming tasks. I think anyone who doesn't work this way is missing the boat, and I think anyone who writes life-critical software without proofs -- and all the other verfication and validations tools available -- is negligent. My point is that I can treat a machine as a Turing machine if it suits my purposes, e.g., if I can't bound a particular algorithm or I want to ignore things like word-length descriptions. But you can't treat a physical realization of a program as having infinite memory for any practical purpose; you only use infinite memory in order to gain insight about computation as a mathematical entity. Even most of the interesting results that come out of computability theory come about because you can bound the size of the tape required according to the size of the input, or some such. (Admittedly, this isn't true of things like the halting problem.) > >I think you missed my point, which is that whether or not the halting >problem can be solved *in theory* for real programs on real computers, >it cannot be solved *in practice*. > >In any case, I don't think that any practical proof methods operate by >treating programs as FSM's. At least one does, or can be read to: see Chapter 0 of Dijkstra's Discipline of Programming. The intuitive model he offers is specifically bounded to finite state spaces. Conveniently, most or all proof methods can ignore bounds on the state space by simply assuming that there is "enough" memory. One of the important points about computability theory in terms of a formal basis for real programming is the computability hierarchy, which establishes bounds on what can be treated as equivalent between FSA's and TM's. This means that one can ignore bounds in many ways; once a program is proven "totally correct" -- which means just that the mapping from inputs to outputs is as specified and the program always halts -- then you are assured that you can bound the size of the machine needed to run the program in a real execution. > >.... The more >complicated and formal the specification, the greater the likelihood >that (a) the customer will believe it and (b) the spec will be wrong. Sure, and that is a real problem. The solution doesn't appear to have a formal basis: there is no algebra of cognition to which we can appeal to "prove" our specifications have read the user's mind. My opinion is that interactive development and prototyping are the only techniques which really give much leverage to this problem. But a formal specification can be based on the behavior of a prototype. A *validation* step can then confirm that the realizaed program behaves the same way as the prototype. > >How about dropping the term "verification" in favor of something that >more accurately describes the state of the art, like "compile-time >assertion-checking" (or, if appropriate, "coding-time assertion >checking" ("semantics-directed editing?!") and "design-time >consistency checking"). How about sending out for pizza and complaining when it doesn't arrive on italian bread? The accepted and standard term for what we're talking about is "verification." The accepted and standard term for confirming the utility of the resulting program and thereby the suitabilty of the requirements as originally stated is "validation." I'm not that hot on verification as a term myself, but there is an existing community that uses the terminology standardly, and they aren't going to change for you or for me. But this is just like the technical term "object." The word has many meanings; however, if you don't complain about the term "object-oriented programming" because the definition of the word "object" requires something that can be seen or felt, all that will happen is that the people who already use the terminology will understand that you don't know the existing work well enough to have a useful opinion. Charlie Martin (crm@cs.duke.edu,mcnc!duke!crm)