Контракт в вашем строительстве не выполняется. Так как вы ссылаетесь на поле объекта (this.data), другие потоки могут иметь доступ к полю и могут изменять его значение между предположением и разрешением первого параметра и разрешением третьего параметра. (например, это могут быть три совершенно разных массива.)
Вы должны присвоить массив локальной переменной, а затем использовать эту переменную в методе. Тогда анализатор узнает, что ограничения выполняются, потому что никакие другие потоки не смогут изменить ссылку.
var localData = this.data;
if (localData == null) return;
byte[] newData = new byte[localData.Length]; // Or whatever the datatype is.
Array.Copy(localData, newData, localData.Length); // Now, this cannot fail.
Это дает дополнительные преимущества не только для удовлетворения ограничения, но, на самом деле, во многих случаях делает код более устойчивым.
Надеюсь, это приведет вас к ответу на ваш вопрос. Я не мог ответить на ваш вопрос напрямую, потому что у меня нет доступа к версии Visual Studio, которая включает в себя статическую проверку. (Я работаю на VS2008 Pro.) Мой ответ основан на том, что мой собственный визуальный осмотр кода завершит, и похоже, что статическая проверка контракта использует аналогичные методы. Я заинтригован! Мне нужно, чтобы получить один из них. : -D
ОБНОВЛЕНИЕ: (множество предположений)
Подумав, я думаю, что могу сделать довольно хорошее предположение о том, что можно или нельзя доказать (даже без доступа к статической проверке). Как указано в другом ответе, статическая проверка не выполняет межпроцедурный анализ. Поэтому, с вероятностью появления многопоточных обращений к переменным (как в OP), статическая проверка может эффективно работать только с локальными переменными (как определено ниже).
Под «локальными переменными» я подразумеваю переменную, к которой не может получить доступ ни один другой поток. Это будет включать в себя любые переменные, объявленные в методе или переданные в качестве параметра, если только параметр не декорирован ref или out или переменная не захвачена анонимным методом.
Если локальная переменная является типом значения, то ее поля также являются локальными переменными (и т. Д. Рекурсивно).
Если локальная переменная является ссылочным типом, то только сама ссылка, а не ее поля, может считаться локальной переменной. Это верно даже для объекта, созданного в методе, поскольку сам конструктор может утечь ссылку на созданный объект (например, статическую коллекцию для кэширования).
Пока статическая проверка не выполняет межпроцедурный анализ, любые предположения, сделанные относительно переменных, которые не являются локальными, как определено выше, могут быть в любое время недействительны и, следовательно, игнорируются в статическом анализе.
Исключение 1: поскольку во время выполнения известно, что строки и массивы являются неизменяемыми, их свойства (например, длина) подлежат анализу, если только переменная строки или массива является локальной. Сюда не входит содержимое массива, которое может изменяться другими потоками.
Исключение 2: может быть известно, что конструктор массива не пропускает никаких ссылок на построенный массив. Поэтому массив, созданный в теле метода и не просочившийся за пределы метода (передаваемый в качестве параметра другому методу, назначенный нелокальной переменной и т. Д.), Имеет элементы, которые также могут рассматриваться как локальные переменные.
Эти ограничения кажутся довольно обременительными, и я могу представить несколько способов, как это можно улучшить, но я не знаю, что было сделано. Вот некоторые другие вещи, которые теоретически можно сделать с помощью статической проверки. Кто-то, у кого это удобно, должен проверить, что сделано, а что нет:
- Он может определить, не вызывает ли конструктор утечки каких-либо ссылок на объект или его поля, и считать поля любого объекта, сконструированного таким образом, локальными переменными.
- Можно провести анализ отсутствия утечек для других методов, чтобы определить, можно ли ссылочный тип, передаваемый методу, все еще считать локальным после вызова этого метода.
- Переменные, украшенные ThreadStatic или ThreadLocal, могут рассматриваться как локальные переменные.
- Могут быть заданы параметры, чтобы игнорировать возможность использования отражения для изменения значений. Это позволило бы считать частные поля только для чтения в ссылочных типах или статические частные поля только для чтения неизменными. Кроме того, когда эта опция включена, закрытая или внутренняя переменная X, к которой only когда-либо обращались внутри конструкции
lock(X){ /**/ } и которая не просочилась, может считаться локальной переменной. Тем не менее, эти вещи, по сути, снизили бы надежность статической проверки, так что это немного сомнительно.
Еще одна возможность, которая может открыть много нового анализа, - это декларативное присвоение переменных и методов, которые их используют (и т. Д. Рекурсивно), для конкретного уникального потока. Это было бы серьезным дополнением к языку, но оно могло бы того стоить.