cline@cheetah.ece.clarkson.edu (Marshall Cline) (01/16/90)
SCENARIO: you're working for MicroS*ft on their new whiz bang C++ compiler (I don't even know if they *have* a C++ compiler :-). You work hard at your assignment (the parser, for example). You tell your boss that you think it works, but you have discovered that your code is in the class of undecidable programs, being transformed from Godel's famous 1931 example. You think your boss will be pleased? I doubt it! Indeed, I doubt *ANYONE* on the entire net has *EVER* written a real-life program which couldn't in theory be verified. We all (well, except for a few of those who posted earlier) know that finding a decision procedure for the predicate calculus (called the "Entscheidungsproblem" and "Hilbert's Program" in various places) is impossible, and therefore the halting problem and program verification are undecidable. But this is a *theoretical* concern which *rarely* impacts our practical "here's a program, boss" world. The fact of the matter is that program verification is *hard*. It's limitation in everyday life is that it's *hard*, not that it's undecidable. Furthermore it *is* semi-decidable. Ie: there exist procedures which will always detect that correct programs *are* correct. The problem is that no *algorithm* can exist for this, since somewhere out there there exist programs which will defy proof (or perhaps they are false but they defy finding a counter-example). So don't think you can't find *anything* via program verification. It's just that you can't find *everything*. Marshall Cline -- _______________________________________________________________________________ Marshall Cline/ECE Department/Clarkson University/Potsdam NY 13676/315-268-3868 cline@sun.soe.clarkson.edu, BH0W@CLUTX (bitnet), uunet!clutx.clarkson.edu!bh0w ==Career search in progress: ECE faculty. Research oriented. Will send vitae.==