Почему этот вызов Contract.Ensure на основе строк не подтвержден?

Question

В моем приложении .Net 4 есть следующий код:

static void Main(string[] args) {
    Func();
}

static string S = "1";

static void Func() {
    Contract.Ensures(S != Contract.OldValue(S));
    S = S + "1";
}

Это дает мне гарантированное недоказанное предупреждение во время компиляции:

warning : CodeContracts: ensures unproven: S != Contract.OldValue(S)

Что происходит?Это прекрасно работает, если S является целым числом.Это также работает, если я изменяю Ensure на S == Contract.OldValue(S + "1"), но это не то, что я хочу делать.

Answer 1

Я предполагаю, что механизм контрактов просто недостаточно умен, чтобы понять, что это гарантировано.Если бы вы сказали:

S = S + "";

... тогда контракт не сработает.Таким образом, движку придется выполнить дополнительную логику, чтобы определить, что S = S + "1" всегда будет менять значение строки.Команда просто не удосужилась добавить эту логику.

Answer 2

Это говорит о том, что Code Contracts не знает, что конкатенация строк с использованием непустой строковой константы всегда будет приводить к другой строке.

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