Dlaczego nie jest sprawdzane połączenie oparte na ciągach znaków Contract.Ensure?

Question

Mam następujący kod w mojej aplikacji .NET 4:

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

static string S = "1"; 

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

Ten Givens mi zapewnia niesprawdzone ostrzeżenie przy kompilacji:

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

Co się dzieje? Działa to dobrze, jeśli S jest liczbą całkowitą. Działa to również, jeśli zmienię opcję Zapewnienie na S == Contract.OldValue(S + "1"), ale nie jest to tym, co chcę zrobić.

Answer 1

Zgaduję, że silnik kontraktów nie jest wystarczająco inteligentny, aby zrozumieć, że jest to gwarantowane. Jeśli powiedziałeś:

S = S + ""; 

... wtedy umowa nie zadziałałaby. Tak więc silnik musiałby wykonać dodatkową logikę, aby ustalić, że S = S + "1" zawsze zmieni wartość ciągu. Zespół po prostu nie doszedł do tego, by dodać tę logikę.

Answer 2

Sugeruje to, że umowy kodowe nie wiedzą, że konkatenacja łańcuchów przy użyciu niepustej stałej łańcuchowej zawsze będzie generować inny ciąg znaków.

To nie jest całkowicie nieuzasadnione, ale możesz zasugerować to zespołowi jako coś, co przyjmie w przyszłych wydaniach.