Le vérificateur statique des contrats de code doit-il être capable de vérifier les limites arithmétiques ?

Question

(Aussi posté sur le forum MSDN - mais qui n'est pas très fréquenté, d'après ce que je peux voir).

J'ai essayé de fournir un exemple de Assert y Assume . Voici le code que j'ai :

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;
}

(La possibilité de transmettre une référence nulle au lieu d'une référence existante). Random La référence est purement pédagogique, bien sûr).

J'avais espéré que si le vérificateur savait que firstRoll y secondRoll étaient chacun dans l'intervalle [1, 6] il serait en mesure de déterminer que la somme est comprise dans la fourchette suivante [2, 12] .

Est-ce un espoir déraisonnable ? Je me rends compte que c'est une affaire délicate, de déterminer exactement ce qui pourrait arriver... mais j'espérais que le vérificateur serait assez intelligent :)

Si ce n'est pas supporté maintenant, est-ce que quelqu'un ici sait si cela va être supporté dans un futur proche ?

EDIT : Je viens de découvrir qu'il existe des options très compliquées pour l'arithmétique dans le vérificateur statique. En utilisant la zone de texte "advanced", je peux les essayer à partir de Visual Studio, mais il n'y a aucune explication décente de ce qu'elles font, pour autant que je puisse dire.

Answer 1

J'ai eu une réponse sur le forum MSDN. Il s'avère que j'y étais presque. En fait, le vérificateur statique fonctionne mieux si vous séparez les contrats "et". Donc, si nous changeons le code en ceci :

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;
}

Cela fonctionne sans aucun problème. Cela signifie également que l'exemple est encore plus utile, car il met en évidence le point précis sur lequel le vérificateur fait fonctionnent mieux avec des contrats séparés.

Answer 2

Je ne connais pas l'outil MS Contracts Checker, mais l'analyse d'intervalle est une technique d'analyse statique standard ; elle est largement utilisée dans les outils d'analyse statique commerciaux pour vérifier que les expressions d'indices sont légales.

MS Research a de bons antécédents dans ce type d'analyse statique, et je m'attends donc à ce que l'analyse de cette gamme soit un objectif du vérificateur de contrats, même si elle n'est pas actuellement vérifiée.