Отсутствие доказательств – не доказательство отсутствия

Отсутствие доказательств – не доказательство отсутствия

Сегодня – ещё два слегка неверных мифа о C#.

Как вы, вероятно, знаете, C# требует, чтобы всем локальным переменным были явно присвоены значения перед тем, как из них читают, но предполагает, что всем полям экземпляра класса изначально присвоены их значения по умолчанию. Порой я слышу такое объяснение причин этого: «компилятор может легко доказать, что локальная переменная не проинициализирована, но значительно труднее доказать отсутствие инициализации для поля экземпляра. И, поскольку конструктор по умолчанию автоматически инициализирует все поля экземпляра значениями по умолчанию, то для полей проводить анализ не нужно».

Оба утверждения слегка неверны.

Первое утверждение неверно потому, что на самом деле компилятор не способен, и не пытается доказать, что локальная переменная неинициализирована. Доказательство этого (1) невозможно, и (2) не даёт нам никакой полезной информации для следующих действий. Невозможно оно потому, что доказательство наличия присваивания значения заданной переменной эквивалентно решению Задачи Останова:

int x;
if (/*тут условие, требующее решения задачи останова*/) x = 10;
print(x);

Если бы мы хотели доказать, что x неинициализирована, то нам бы во время компиляции пришлось бы доказать ложность условия. Наш компилятор не настолько изощрён!

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

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

int x, y = 0;
if (0 * y == 0) x = 10;
print(x);

Мы с вами знаем, что x определённо инициализирована, но в C# 3 компилятор осознанно недостаточно умён, чтобы это доказать. (Занятно, что он был достаточно умён в C# 2. Я сломал это, чтобы привести компилятор в соответствие со спецификацией; быть умнее в противоречие спецификации не всегда хорошо.)

Этот пример снова демонстрирует, что мы не доказываем неинициализированность x; если бы мы это доказали, то наша доказывалка содержала бы ошибку, так как мы с вами знаем, что x определённо инициализирована. Скорее, нам не удаётся доказать, что x инициализирована.

Это интересный вариант спора между скептиками и легковерами, который происходит следующим образом: скептик говорит «нет надёжных подтверждений существования йети, так что йети не существует». Легковер отвечает «отсутствие подтверждения не является подтверждением отсутствия; так что да, йети существуют». В обоих случаях, рассуждения с позиций отсутствия надёжных подтверждений редко приносят пользу! Но в нашем случае, именно потому, что нам не хватает надёжных подтверждений, мы и приходим к выводу, что наших знаний недостаточно, чтобы позволить вам читать x.

(Принцип, позволяющий на основе отсутствия надёжного подтверждения сделать предварительное заключение о мифичности йети – «экстраординарные утверждения требуют экстраординарных подтверждений». Разумно предполагать, что экстраординарное утверждение ложно, до получения надёжного подтверждения. Когда чрезвычайно надёжное подтверждение находится для экстраординарного утверждения – например, экстраординарного утверждения о том, что само время замедляется, когда ты движешься быстрее, - то имеет смысл поверить в это экстраординарное утверждение. Чрезвычайно надёжные подтверждения были получены для теории относительности, но не для теории йети.)

Второй миф в том, что конструктор по умолчанию инициализирует поля их значениями по умолчанию. Это можно опровергнуть несколькими аргументами.

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

Во-вторых, даже если у класса есть конструктор по умолчанию, то нет гарантии, что он будет вызван. Может быть использован какой-то другой конструктор.

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

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

На самом деле происходит то, что аллокатор памяти CLI гарантирует, что память, выделенная экземпляру класса, будет вся инициализирована нулями до того, как произойдёт вызов конструктора. К моменту, когда запускается конструктор, объект уже свежеобнулён и готов ко всему.