Xref: utzoo comp.ai:5581 comp.edu:2926 comp.object:758 Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cs.utexas.edu!swrinde!ucsd!ucbvax!hplabs!otter!hplb!cdollin!kers From: kers@hplb.hpl.hp.com (Kers) Newsgroups: comp.ai,comp.edu,comp.object Subject: Re: Re^2: Reasons why you don't prove your programs are correct Message-ID: Date: 16 Jan 90 14:18:46 GMT References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <16479@joshua.athertn.Atherton.COM> <166 Sender: news@hplb.hpl.hp.com Organization: Hewlett-Packard Laboratories, Bristol, UK. Lines: 105 In-reply-to: joshua@athertn.Atherton.COM's message of 15 Jan 90 18:41:00 GMT joshua@athertn.Atherton.COM (Flame Bait) writes: | kers@hplb.hpl.hp.com (Kers) [that's me] writes: | >I'll also think that the remark "specifying most programs is impossible" is | >wrong. "bloody difficult, especially after the fact" is the predicate that | >springs to mind. | | No problem. Specifiy the following programs, in a machine readable | format useful to a program verifier. These should be commerical products, | so they must look good and feel good so that people want to use them: Let me admit that I don't have a verifier to hand, so the machine-readability of any specification I might supply is a little beside the point. (There are any number of specification languages one might use, with varying degrees of accessibilility and surface-level checking.) Let me also admit that "look good" and "feel good" are things I have no idea how to specify. Can we agree that much of the program behaviour is independent of the look-and-feel? [Lest this should seem a cop-out, there's no reason why one shouldn't specify the "look" in a formal fashion. It's just that "looking good" would have to be a property that was asserted about particular - eg - screen layouts; it can't be derived from mathematics. I just happen to think that this isn't a particularly important problem *for verification* - it's part of the harder problem of whether the specification is *appropriate* to the problem at hand. Discussion encouraged.] | A rule based expert system shell. | Remember to specify input and output for an window based system. What makes the I/O for a window system harder than for a terminal? | A source code control facility like SCCS or RCS | If you use system calls you must have some way of proving that | they do what your spec says they do. No, *I* don't. I hope *someone* has; one day I'd like there to be a formal proof that they *do* do what they're supposed to. The behaviour of system calls is given, like the behaviour of "+"; the correctness of the program is relative to the correctness of the system calls. In fact, I can state the correctness of the program in just those relative terms; *if* these system calls S1 ... Sn have meanings M1 ... Mn, then the program is correct (has the specified behaviour). You can then examine my assumptions about the system and decide whether they are justified. | | | My last example points out a current problem with proving program correct. | They must only use libraries which have been proven correct, must run on | an operating system which has been proven correct, and must use hardware | which is proven correct. All of this is impossible right now. True, but ... it depends what you're trying to accomplish. I agree that if we demand complete proofs - in the sense that the proof extends all the way to the bedrock - we can't do it [ever - see [*1]]. If we're happy to prove things relative to some set of base assumptions (system calls behave this way, and if they don't it's the system call that's broken, not the program) we can practice separation of concerns. | I'm serious about this challenge. I hold that these program can not | be specified in any kind of useful way, and that the set of programs How much specification is enough? How little would help? In the case of the expert system shell, surely a specification of the inference engine (and a proof that the code satisfied it) would be useful, even if the I/O was on shaky ground. After all, if the system misbehaved, you could concentrate your efforts away from the engine. | which can be proven correct is so small as to be uninteresting. Before I disagree any more I think we ought to decide just what limits we're prepared (or not) to place on specifications and proofs. For example, do you think that specifying a "real world program" is *in principle* impossible; if so, why? Or just that it cannot be done *now*? Do you think that working on verification is a complete waste of time, or just that some of its proponents are hypemasters? Would proofs of components strike you as an improvement over no proofs at all, or do you want the whole cat in the bag? -- Footnoties follow ---------------------------------------------------------- [*1] You can't prove hardware correct; its behaviour is physics. You can only prove it relative to your assumptions about the physics of electrons in semiconductors (or whatever). Similarly, you can't prove that an expert system is "correct", if by that you mean that it gives genuinely "expert" answers. But you could show that it will give answers that are derivable (in whatever sense is appropriate) from its rulebase. Proving that the rulebase has some correspondance with reality is *not* program verification. -- Regards, Kers. "If anything anyone lacks, they'll find it all ready in stacks."