This is a mirror of official site: http://jasper-net.blogspot.com/

Never Say Never, Part Two

| Sunday, March 6, 2011
Whether we have a "never" return type or not, we need to be able to determine when the end point of a method is unreachable for error reporting in methods that have non-void return type. The compiler is pretty clever about working that out; it can handle situations like

int M()
{
  try
  {
    while(true) N();
  }
  catch(Exception ex) 
  { 
    throw new WrappingException(ex); 
  }
}

The compiler knows that N either throws or it doesn't, and that if it doesn't, then the try never exits, and if it does, then either the construction throws, or the construction succeeds and the catch throws. No matter what, the end point of M is never reached.

However, the compiler is not infinitely clever. It is easy to fool it:

int M()
{
  int x = 123;
  try
  {
    while(x >= x / 2) x = x / 2;
  }
  catch(Exception ex) 
  { 
    throw new WrappingException(ex); 
  }
}

Here x is always going to be a small, non-negative integer, and a small, non-negative integer is always greater than or equal to half of it. You know that, I know that, but the compiler doesn't know that. The compiler complains that this method has a reachable end point, even though clearly the end point will never be reached. We could put that logic into the compiler if we really wanted to; we could be more clever.

How much more clever could we be? Is there any limit to our cleverness? Could we in theory produce a compiler that perfectly determined whether the end point of a method was reachable?

Turns out, no. A proof of that fact is a bit tricky, but we're tough, we can do it.

First off, let's restrict the problem to a particular pattern. Consider programs of this form:

class Program
{
  private static string data = @"some data";
  public static int DoIt()
  {
     some code
  }
}

The question is "given values for 'some data' and 'some code', does DoIt have a reachable end point?" If we can't solve the problem for programs with this very restrictive format then we can't solve it in general, so let's explore whether we can solve problems in this limited format.

Posted via email from Jasper-net

0 comments: