Warum ist dieser auf Strings basierende Contract.Ensure-Aufruf nicht bewiesen?

Question

Ich habe den folgenden Code in meinem .Net 4 App:

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

static string S = "1"; 

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

Dieses givens mich ein bei der Kompilierung nicht bewiesen Warnung gewährleistet:

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

Was ist los? Dies funktioniert gut, wenn S eine ganze Zahl ist. Es funktioniert auch, wenn ich die Sicherung auf S == Contract.OldValue(S + "1") ändere, aber das ist nicht, was ich tun möchte.

Answer 1

Ich rate der Kontraktmotor ist einfach nicht schlau genug zu verstehen, dass dies garantiert ist. Wenn Sie gesagt hätten:

S = S + ""; 

... dann würde der Vertrag nicht funktionieren. Daher müsste die Engine eine zusätzliche Logik ausführen, um zu bestimmen, dass S = S + "1" immer den Wert der Zeichenfolge ändert. Das Team ist einfach nicht dazu gekommen, diese Logik hinzuzufügen.

Answer 2

Das deutet darauf hin, dass Code Contracts nicht wissen, dass String-Verkettung mit einer nicht leeren String-Konstante immer eine andere Zeichenfolge erzeugen wird.

Das ist nicht ganz unvernünftig, aber Sie könnten es dem Team als etwas vorschlagen, das sie für zukünftige Versionen übernehmen.