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


(También publicado en el foro de MSDN - pero eso no tiene mucho tráfico, por lo que puedo ver).

He estado tratando de dar 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 poder pasar una referencia nula en lugar de una existente Random la referencia es puramente pedagógica, por supuesto).

Tenía la esperanza de que si el inspector sabía eso firstRoll y secondRoll estaban cada uno en el rango [1, 6], sería capaz de calcular que la suma estaba en el rango [2, 12].

¿Es esto una esperanza irracional? Me doy cuenta de que es un asunto complicado, averiguar exactamente qué podría pasar ... pero esperaba que el inspector fuera lo suficientemente inteligente :)

Si esto no es compatible ahora, ¿alguien sabe aquí si es probable que sea compatible en un 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é.


32
2017-08-07 11:38


origen


Respuestas:


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". Entonces, si cambiamos el código a esto:

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 mismo punto que el verificador hace trabaje mejor con contratos separados.


14
2017-08-07 20:27



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 el análisis de rango sea un objetivo del Contracts Checker, incluso si no se comprueba actualmente.


1
2017-08-07 14:10