c# - ¿Cómo funciona Contract.Seguros?

code-contracts

Question

Estoy empezando a usar los Contratos de Código, y aunque Contract.Requires es bastante sencillo, tengo problemas para ver lo que Asegura realmente hace.

He intentado crear un método simple como este:

static void Main()
{
DoSomething();
}
private static void DoSomething()
{
Contract.Ensures(false, "wrong");
Console.WriteLine("Something");
}

Sin embargo, nunca veo el mensaje "incorrecto", ni lanza excepciones ni nada más.

Entonces, ¿qué es lo que realmente hace?

Answer 1

Es extraño que no lance nada, si está ejecutando la herramienta de reescritura con la configuración adecuada. Mi conjetura es que está ejecutando en un modo que no comprueba las condiciones posteriores.

Lo confuso de Contract.Ensures es que lo escribe al inicio del método, pero se ejecuta al final del método. El reescritor hace toda la magia para asegurarse de que se ejecuta correctamente, y se le da el valor de retorno si es necesario.

Al igual que muchas cosas sobre los contratos de código, creo que es mejor ejecutar Reflector en los resultados de la herramienta de reescritura. Asegúrese de que tiene la configuración correcta, luego averigüe qué ha hecho el reescritor.

EDITAR: Me doy cuenta de que no he expresado el punto de Contact.Ensures . Contact.Ensures todavía. En pocas palabras, es para asegurarse de que su método haya hecho algo al final, por ejemplo, podría asegurar que se agregue algo a una lista, o (más probablemente) que el valor de retorno no sea nulo, positivo o lo que sea. Por ejemplo, podría tener:

public int IncrementByRandomAmount(int input)
{
// We can''t do anything if we''re given int.MaxValue
Contract.Requires(input < int.MaxValue);
Contract.Ensures(Contract.Result<int>() > input);
// Do stuff here to compute output
return output;
}

En el código reescrito, habrá una verificación en el punto de retorno para garantizar que el valor devuelto sea realmente mayor que la entrada.