Xref: utzoo comp.ai:5500 comp.edu:2895 comp.object:726 Path: utzoo!attcan!uunet!aplcen!uakari.primate.wisc.edu!uwm.edu!zaphod.mps.ohio-state.edu!usc!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: 12 Jan 90 14:34:44 GMT References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <16479@joshua.athertn.Atherton.COM> Sender: news@hplb.hpl.hp.com Organization: Hewlett-Packard Laboratories, Bristol, UK. Lines: 45 In-reply-to: joshua@athertn.Atherton.COM's message of 12 Jan 90 01:29:37 GMT joshua@athertn.Atherton.COM (Flame Bait) writes: | "Proving your programs are correct" seems to mean different things | to different people: | One group thinks it means that your program does exactly what your | spec says it should. ... | The first sort of proof is obviously useless, the spec becomes the | program, and bugs in the spec become bugs in the program. Also, | specifing most programs is impossible; and if you could, then you | could write a compiler for the specification language. I've seen this kind of remark several times in this multi-group discussion. *It just isn't true*. Just because you can write a specification for a program doesn't mean you can write a compiler for the specification language which generates code, let alone acceptably efficient code. Suppose I specify an square root function "sqrt" by: abs( sqrt( x ) ** 2 - x ) < 0.01 [Er - I'm not a numerical analyst; this fixed bound of 0.01 looks very suspect to me, and I suspect that it's not the right kind of specification. But this is a different issue.] I claim this is a good specification (modulo the [...]) of the behaviour of "sqrt". Now tell me how you're going to generate code for sqrt from it, and convince me that the code will be efficient, and that you have a *general* mechanism that will do this for examples further removed from the Opening Book of moves in the Specification Game. 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. Regards, Kers. -- Regards, Kers. "If anything anyone lacks, they'll find it all ready in stacks."