¿Debería el verificador estático de contratos de código ser capaz de verificar el límite aritmético?

Question

(también posted on the MSDN forum - pero que no recibe mucho tráfico, por lo que yo puedo ver.)

He estado tratando de proporcionar un ejemplo de Assert y Assume. Aquí está el código que tengo:

public static int RollDice(Random rng) 
{ 
    Contract.Ensures(Contract.Result<int>() >= 2 && 
        Contract.Result<int>() <= 12); 

    if (rng == null) 
    { 
     rng = new Random(); 
    } 
    Contract.Assert(rng != null); 

    int firstRoll = rng.Next(1, 7); 
    Contract.Assume(firstRoll >= 1 && firstRoll <= 6); 

    int secondRoll = rng.Next(1, 7); 
    Contract.Assume(secondRoll >= 1 && secondRoll <= 6); 

    return firstRoll + secondRoll; 
} 

(El negocio de ser capaz de pasar de una referencia nula en lugar de una referencia existente Random es puramente pedagógica, por supuesto.)

yo esperaba que si el inspector sabía que firstRoll y secondRoll estaban cada uno en el rango [1, 6], se podría deducir que la suma estaba en el rango [2, 12].

¿Es esta una esperanza irracional? Me doy cuenta de que es un asunto complicado, resolver exactamente lo que podría pasar ... pero esperaba que el verificador fuera lo suficientemente inteligente :)

Si esto no es compatible ahora, ¿alguien sabe aquí si es probable que sea compatible? en el futuro cercano?

EDITAR: Ahora he encontrado que hay opciones muy complicadas para la aritmética en el comprobador estático. Usando el cuadro de texto "avanzado" puedo probarlos desde Visual Studio, pero no hay una explicación decente de lo que hacen, hasta donde sé.

Answer 1

He tenido una respuesta en el foro de MSDN. Resulta que estaba muy cerca de allí. Básicamente, el verificador estático funciona mejor si se dividen los contratos "editados". Por lo tanto, si cambiamos el código a este:

public static int RollDice(Random rng) 
{ 
    Contract.Ensures(Contract.Result<int>() >= 2); 
    Contract.Ensures(Contract.Result<int>() <= 12); 

    if (rng == null) 
    { 
     rng = new Random(); 
    } 
    Contract.Assert(rng != null); 

    int firstRoll = rng.Next(1, 7); 
    Contract.Assume(firstRoll >= 1); 
    Contract.Assume(firstRoll <= 6); 
    int secondRoll = rng.Next(1, 7); 
    Contract.Assume(secondRoll >= 1); 
    Contract.Assume(secondRoll <= 6); 

    return firstRoll + secondRoll; 
} 

Eso funciona sin ningún problema. También significa que el ejemplo es aún más útil, ya que resalta el punto en que el verificador hace que funciona mejor con contratos separados.

Answer 2

No conozco la herramienta MS Contracts Checker, pero el análisis de rango es una técnica estándar de análisis estático; es ampliamente utilizado en herramientas comerciales de análisis estático para verificar que las expresiones de subíndices sean legales.

MS Research tiene una buena trayectoria en este tipo de análisis estático, por lo que espero que dicho análisis de rango sea un objetivo del Comprobador de contratos, incluso si no está verificado actualmente.