Re: What Can We Do About Unprovable Errors?
Posted: Jun 25, 2004 11:58 AM
Andrew Koenig wrote:
>Now, suppose this expression is compiled separately from
>the definitions of incr and decr. The compiler cannot
>possibly tell that incr and decr happen to make this
>expression's behavior undefined, because it may be that I
>haven't even written incr and decr yet. So if the error is
>to be detected at all, it will have to be in the linker.
The compiler can warn about code that involves unspecified behaviour (like order of evalation). That way, you get a warning about it, even if it doesn't tell you whether or not what you're doing ends up as undefined behaviour (relying on a certain order of evaluation).
Thus, you ignore the warning at your own peril - that is, you rely on the order at your own peril. The Intel C++ compiler has this warning for expressions and evaluation of function arguments. Unfortunately, as lots of places in the code may involve unspecified behaviour, the warning isn't really useful if you know what you're doing and don't rely on the order. However, for beginners, it might be a useful reminder.
I don't really think - at least this particular issue (order of evaluation) - is much of an issue. More experienced people knows about it, and it becomes second nature, and it's similar to not reading from or writing to an object more than once between sequence points (if you write int i=0; i=++i;, you get what you deserve. ;) ).
As I understand, these various unspecified/undefined behaviours are there for reasons of efficiency (like being able to reorder an expression for evaluation), and I don't think we should lightly change that. However, as shown with the compiler warnings, there may still be warnings about potetial undefined behaviour.
As an aside, it seems to me that this is more about "untestable errors" (cannot be relied on as correct, even if the test passes), rather than "unprovable errors". Testing and proof (in the mathematical sense) are rather different things. After all, you can't be sure to find the errors in testing, but you theoretically can find them, using whole-program analysis (proof).