Контракты кода.NET: может ли он стать более базовым, чем этот?

Question

Я просто возился, чтобы ответить на чей-то вопрос здесь, о переполнении стека, когда я заметил предупреждение о статической проверке изнутри моей Visual Studio (2008):

string[] source = { "1", "A", "B" };
var sourceObjects = Array.ConvertAll(source, c => new Source(c)).ToArray();

Я получаю сообщение требует недоказанного источника!= Ноль. Мне кажется довольно очевидным, что это не так. Это всего лишь один пример, конечно. С другой стороны, некоторые изящные вещи, кажется, работают довольно хорошо.

Я использую релиз 1.2.20518.12 (18 мая). Я нахожу контракты кода очень интересными, но у кого-нибудь еще были подобные случаи? Считаете ли вы текущую реализацию пригодной для использования на практике, или вы считаете ее чисто академической на данный момент?

Я сделал это вики-сообществом, но я хотел бы услышать некоторые мнения:)

Answer 1

Это имеет больше смысла, если вы разделите два вызова:

string[] source = { "1", "A", "B" };
var tmp = Array.ConvertAll(source, c => new Source(c));
var sourceObjects = tmp.ToArray();

Теперь он указывает на последнюю строку как проблему. Другими словами, призыв к Array.ConvertAll знает, что источник не является нулевым, но вызов ToArray() не знает что tmp не будет нулевым

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

В принципе, я считаю, что все это будет работать, когда Array.ConvertAll получит соответствующее пост-условие ненулевого значения. До тех пор, это сделает свое дело:

string[] source = { "1", "A", "B" };
var tmp = Array.ConvertAll(source, c => new Source(c));
Contract.Assume(tmp != null);
var sourceObjects = tmp.ToArray();

Я согласен, что такие вещи раздражают, но я уверен, что они быстро улучшатся, поскольку MS добавляет все больше и больше контрактов в BCL. Важно отметить, что это не проблема самой статической проверки.

(По факту, Array.ConvertAll не имеет предварительного условия - если вы установите source переменная нуль во втором фрагменте кода выше, он все равно не будет жаловаться.)