¿Por qué no se prueba esta llamada Contract.Ensure basada en cadenas?

Question

Tengo el siguiente código en mi aplicación .Net 4:

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

static string S = "1"; 

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

Esto me givens una advertencia asegura no probada en tiempo de compilación:

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

¿Qué está pasando? Esto funciona bien si S es un número entero. También funciona si cambio Asegurar a S == Contract.OldValue(S + "1"), pero eso no es lo que quiero hacer.

Answer 1

Supongo que el motor de contratos simplemente no es lo suficientemente inteligente como para entender que esto está garantizado. Si hubiera dicho:

S = S + ""; 

... entonces el contrato no funcionaría. Entonces, el motor tendría que hacer un poco de lógica adicional para determinar que S = S + "1" siempre cambiará el valor de la cadena. El equipo simplemente no ha logrado agregar esa lógica.

Answer 2

Eso sugiere que Code Contracts no sabe que la concatenación de cadenas que utiliza una constante de cadena no vacía siempre producirá una cadena diferente.

Eso no es enteramente irrazonable, pero es posible que desee sugerirle al equipo como algo que asumen para futuras versiones.