Limitations and Evolution [LWN.net]

Limitations and Evolution

Posted Apr 4, 2006 19:30 UTC (Tue) by nix (subscriber, #2304)
In reply to: Limitations and Evolution by iabervon
Parent article: Coverity: one bug fixed every six minutes

Unfortunately you don't need particularly contrived code to collide with Rice's theorem, in my experience :( even static checkers will frequently need to say `oh, I give up' and not warn about it, at least for some classes of test.

I wish this wasn't true. I want a better universe: this one's broken.

to post comments

Limitations and Evolution

Posted Apr 4, 2006 20:15 UTC (Tue) by iabervon (subscriber, #722) [Link]

I think that's not so much a consequence of Rice's theorem as an effect of not supporting quite all of the sorts of constraints programmers use. A bigger issue is that, even for decidable questions of interest (e.g., is there a proof of the correctness of this code which would fit on a single page?) they're often NP-complete. So you get code with a comment explaining why it's okay, and programmers can check that it's true in polynomial time, but the static checker can't come up with the correct rule in a reasonable time (and, of course, the original programmer came up with the constraint first and then wrote the code to obey it). But that's an issue of feasibility, not decidability. This can be made practical with annotations and assertions, although these have to be made acceptable to programmers by being sufficiently readable and writable (so the programmer can write them without much trouble, and so other programmers find them helpful in understanding why the code works).

And, of course, a static checker is only really useful when the number of cases it fails to complete which people can tell are okay is low enough that it can usefully flag as flaws everything that it can't prove.