Perché questo contratto basato su stringhe.Esure non è stato verificato?

Question

Ho il seguente codice nel mio .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"; 
} 

Questo mi givens un avvertimento garantisce non provata in fase di compilazione:

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

Che cosa sta succedendo? Funziona bene se S è un numero intero. Funziona anche se cambio l'Assicurare su S == Contract.OldValue(S + "1"), ma non è quello che voglio fare.

Answer 1

Immagino che il motore dei contratti non sia abbastanza intelligente da capire che questo è garantito. Se avessi detto:

S = S + ""; 

... allora il contratto non funzionerebbe. Quindi il motore dovrebbe fare qualche logica in più per determinare che S = S + "1" cambierà sempre il valore della stringa. Il team semplicemente non è riuscito ad aggiungere quella logica.

Answer 2

Ciò suggerisce che i Contratti di codice non sanno che la concatenazione di stringhe utilizzando una costante di stringa non vuota produrrà sempre una stringa diversa.

Questo non è interamente irragionevole, ma si potrebbe desiderare di suggerirlo al team come qualcosa che assumono per le versioni future.