Weblogs Forum - What Can We Do About Unprovable Errors?

Articles |
News |
Weblogs |
Books |
Forums

Artima Forums | Articles | Weblogs | Java Answers | News

Sponsored Link •

Weblogs Forum
What Can We Do About Unprovable Errors?

19 replies on 2 pages. Most recent reply: Jun 25, 2004 12:37 PM by Andrew Koenig

Welcome Guest
Sign In

Back to Topic List

Reply to this Topic

Search Forum

Threaded View


Previous Topic		Next Topic

Flat View: This topic has 19 replies on 2 pages [ « | 1 2 ]

Michael Feathers

Posts: 448
Nickname: mfeathers
Registered: Jul, 2003

Re: What Can We Do About Unprovable Errors?

Posted: Jun 16, 2004 3:42 PM

> My experience,
> however, is that it is not possible to be able to count on
> programmers following it consistently in practice. The
> number of things one has to remember is just too large. I
> would like to be able to use mechanical means to make that
> number smaller.

It seems that the border between provable and unprovable is slippery. I remember developing a library that was tested under Zortech, Watcom, Microsoft, Borland and a couple of other C++ compilers to assure the same results.

It seems like the largest class of unprovables has to do with portability across implementations. What is left? Is threading the only one?

Andrew Koenig

Posts: 10
Nickname: ark
Registered: Apr, 2003

Re: What Can We Do About Unprovable Errors?

Posted: Jun 16, 2004 8:45 PM

> It seems like the largest class of unprovables has to do
> with portability across implementations. What is left?
> Is threading the only one?

Any program that evokes undefined behavior has an unprovable error, because even if you can write a test that reliably reproduces the problem, there is no guarantee that it will not start appearing to work in the future.

So, for example, unprovable errors include buffer overruns, dangling pointers, integer overflow or underflow, and programs that depend on order of evaluation.

Gregg Wonderly

Posts: 317
Nickname: greggwon
Registered: Apr, 2003

Re: What Can We Do About Unprovable Errors?

Posted: Jun 17, 2004 10:29 AM

If the compiler had access to the source for all of this at once, it could of course reduce the expression to something like

   ++x + --x;

which could be established to reference the same variable with modification happening between references. The compiler could then assert that this expression produces undefined results.

Andrew, I think the other interesting step would be for the linker to get involved. But, that doesn't solve the shared library references that wouldn't be established until runtime and which would allow the causual relationship to be known.

Your example is a producedural example where strict code analysis is easier. If it was OO, then the exact version of incr() and decr() and the semantics of their actions would not be visible until the moment of the call. So, it would be more difficult to do the analysis.

But, I think there are some interesting things to imagine. Java has a bunch of meta-data conveyences such as Javadoc and the new annotations. If the compiler annotated the byte codes of the called methods to say which variables they modified and referenced, and the classloader/resolver new expression boundries, it might be possible for the first pass through the execution, that some extreme analysis could be performed to check for 'changed during reference'.

But, there are several other class of unprovable errors that are related to ordering. Threading introduces a wide range of complications that all of us deal with day in and day out in Java. But, it has become old hat for me. I always think about every class and method I create, imagining that any thread from any context could call it, and think about creating idempotent behavior too. I've been usig RMI and Jini for remote services for years, and even that environment presents the issue of unprovable errors.

Terje Slettebø

Posts: 205
Nickname: tslettebo
Registered: Jun, 2004

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).

Regards,

Terje

Andrew Koenig

Posts: 10
Nickname: ark
Registered: Apr, 2003

Re: What Can We Do About Unprovable Errors?

Posted: Jun 25, 2004 12:37 PM

> The compiler can warn about code that involves
> unspecified behaviour (like order of evalation).

The compiler can warn about some such code, but not all. At least not unless you want to get a lot of spurious warnings.

> I don't really think - at least this particular issue
> (order of evaluation) - is much of an issue.

It is usually not much of an issue. I picked it merely as one example among many.

> 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.

That's exactly the problem: In exchange for this kind of efficiency, we get programs that may conceal errors that can never be assuredly found by testing.

> 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).

I thought for a long time about whether to use the term "untestable" rather than "unprovable", and decided not to do so because in fact the errors might well be testable. The distinction is subtle: I am not talking about errors that tests cannot reveal, but rather about errors that tests cannot be assured of revealing. It might well be that some other test could reveal the error, if only you knew what that test was.

Also, I am not convinced that you can find every error in every program through whole-program analysis, even in theory. Because just as Goedel's Theorem shows that there are some statements that are true even though it is impossible to prove them, I suspect that there must also be programs that are correct even though it is impossible to find a proof that they are correct. If that is true, then the inability to prove that a program is correct does not prove it incorrect.

Flat View: This topic has 19 replies on 2 pages [ « | 1 2 ]

Previous Topic

Next Topic


	Web Artima.com