Freigeben über


Никогда не говори никогда. Часть 2

Независимо от того, есть ли у нас тип возвращаемого значения «never» (никогда) или нет, для выдачи сообщения об ошибке, нам нужно определить, является ли конечная точка метода достижимой для методов, возвращающих значения. Компилятор достаточно умен для определения такой ситуации; например, он может справиться со следующим примером:

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

Компилятор знает, что если метод N не сгенерирует исключение, то блок try никогда не завершится, а если сгенерирует исключение, то оно будет перехвачено блоком catch и будет сгенерировано другое исключение. Независимо ни от чего, конечная точка метода M недостижима.

Однако компилятор не бесконечно умен. Его весьма просто надуть:

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

В этом примере, переменная x будет маленьким неотрицательным целым, а маленькое неотрицательное целое всегда больше или равно своей половине. Вы это знаете, я это знаю, но компилятор этого не знает. В данном случае компилятор будет жаловаться, что конечная точка метода достижима, хотя ясно, что это не так. Если захотим, мы можем добавить эту логику в компилятор и сделать его умнее.

Насколько умнее он может быть? Где предел этому? Можем ли мы, хотя бы теоретически, создать компилятор, который сможет четко определять, достижима ли конечная точка метода?

Оказывается, что нет. Доказать это не так просто, но мы сможем это сделать.

Прежде всего, давайте ограничим нашу задачу определенным шаблоном. Давайте рассмотрим программу следующего вида:

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

Вопрос следующий: «если значения ‘ somedata ’ и ‘ somecode ’ известны, достижима ли конечная точка метода DoIt ? ». Если мы не сможем решить эту задачу для программы с такими жесткими ограничениями, тогда мы не сможем решить эту задачу в общем случае. Так что, давайте выясним, сможем ли мы решить эту задачу в такой ограниченной форме.

Давайте предположим, что в библиотеке компилятора у нас есть класс с открытым методом, отвечающим на этот вопрос. Мы предполагаем, что “code” является корректной C# программой, а “data” содержит корректный строковый литерал.

 public class Compiler
{
  public static bool HasReachableEndPoint(string code, string data)
  {
    // [Код пропущен: вычислить результат и вернуть это значение]
  }
}

А вот тут начинаются сложности. Что если мы вызываем следующий код:

 string weird = @"
if (Compiler.HasReachableEndPoint(data, data))
  return 123;
";
bool result = Compiler.HasReachableEndPoint(weird, weird);

Что делает этот код? Он пытается определить, является ли конечная точка метода DoIt достижимой в следующей программе:

class Program
{
  private static string data = @"
if (Compiler.HasReachableEndPoint(data, data))
  return 123;
";
  public static int DoIt()
  {
     if (Compiler.HasReachableEndPoint(data, data))
       return 123;
  }
}

И каков результат выполнения? Предположим, результатом вызова является true. Это означает, что конечная точка метода DoIt достижима. Что, в свою очередь, означает, что при вызове метода DoIt результатом условного выражения является false. Но строки “data” и “weird” одинаковы, так как «результат» может быть true, когда результат вызова этой же функции должен вернуть false? Это логически непоследовательно, поэтому результат не может быть равен true. Очевидно, что я не могу выпить из ближней чашки.

Предположим, «результат» равен false. Это значит, что конечная точка метода DoIt недостижима. А это означает, что метод Compiler.HasReachableEndPoint(data, data) всегда либо возвращает true, генерирует исключение или выполняется бесконечно. Но, опять-таки, “data” и “weird” – это одна и та же строка, так почему этот метод вернет true, сгенерирует исключение, или будет выполняться вечно, если мы предполагаем, что при заданных входных параметрах он возвращает false? Очевидно, результат также не равен “false”, поскольку это также ведет к противоречию. Очевидно, я не могу выпить из ближайшей к вам чашки.

Поскольку результат не может быть ни true, ни false, метод HasReachableEndPoint для заданных входных данных должен либо генерировать исключение, либо выполняться бесконечно. Но если это так, тогда наш метод для определения достижимости конца метода, может приводить к тому, что компилятор будет падать или выполняться вечно, а это плохо. Компилятор должен уметь компилировать любые корректные программы, даже безумные.

Это показательный пример того, что вы не должны становиться на пути сицилийца, когда речь идет о его смерти, так и наш метод проверки достижимости конца метода логически должен либо (1) иногда возвращать неправильный результат или (2) не давать результат вовсе. Проблема достижимости конца метод в общем случае не может быть решена компилятором надежным образом, независимо от того, насколько умны его разработчики.

Теперь вы можете отталкиваться от этого доказательства, заметив, что это обоснование основывается на абсолютно сумасшедшей ситуации, когда программа содержит часть своего собственного кода в виде данных, в которые, в свою очередь, вызывают анализатор достижимости. Дуглас Хофстедер (Douglas Hofstadter) назвал подобную ситуацию «странным циклом» (strange loop). Даже если вам это доказательство не нравится, у нас есть другие доказательства того, что «идеальный» определитель достижимости конечной точки метода, всегда возвращающий корректный результат за конечное время, видимо, невозможен. В качестве примера, давайте рассмотрим очень простой маленький метод, с пятью циклами и некоторыми вычислениями с целочисленными типами произвольной точности:

 public static int DoIt()
{
  Integer max = 0;
  while(true)
  {
    max += 1;
    for (Integer x = 1; x <= max; ++x)
      for (Integer y = 1; y <= max; ++y)
        for (Integer z = 1; z <= max; ++z)
          for (Integer n = 1; n <= max; ++n) 
            if (x.Power(n+2) + y.Power(n+2) == z.Power(n+2)) goto done;
  }
  done: ;
  // Упс, мы «забыли» вернуть int.
  // Однако это является проблемой, только если эта метка достижима.
}

Хотите узнать, справедлива ли последняя теорема Ферма? Просто запустите волшебный идеальный компилятор для класса, содержащего этот метод, и посмотрите, скомпилируется ли он. Если он выдаст ошибку «конечная точка метода, возвращающего значение, достижима», тогда оператор goto достижим. Это значит, что существует решение этого уравнения и последняя теорема Ферма ошибочна. Если компиляция завершится успешно (с выдачей предупреждения о недостижимой метке!), тогда оператор goto недостижим и теорема верна. Для ответа на этот вопрос вам даже не нужно запускать саму программу, вам достаточно ее откомпилировать! Тот факт, что эта программа безумно неэффективна из-за количества вычислений, совершенно не важен, поскольку мы даже не собираемся ее запускать.

Такой компилятор позволяет нам найти ответ на любой открытый вопрос конечной математики путем простого написания программы, которая прерывает свое выполнение, если это предположение верно и выполняется вечно, если нет. Кажется немыслимым, что мы можем, хотя бы теоретически, написать компилятор, способный давать ответы на неразрешенные вопросы за всю историю конечной математики.

Эта известная проблема носит название «проблемы остановки» (Halting Problem), поскольку она обычно возникает в вычислительных системах, которые не содержат «генерацию исключения», как варианта исполнения. В таких системах существует лишь два варианта выполнения – «прервать выполнение с некоторым результатом» или «выполняться в бесконечном цикле».

Проблема остановки, конечно же, решаема с помощью эвристик, обеспечивающих терпимое количество ложных положительных результатов ( falsepositive ) . Компилятор C# с радостью скажет вам, когда конечная точка метода гарантированно недостижима, но как мы видели, вы можете обмануть его, в результате чего он скажет вам, что некоторая недостижимая точка является достижимой. До тех пор, пока у вас не будет ложных отрицательных результатов (false negative) (т.е. когда компилятор скажет вам, что некоторая достижимая конечная точка метода является недостижимой) все в порядке.

Оригинал статьи