le code des marchés vérificateur statique doit être en mesure de vérifier lié arithmétique?

Question

(également affichée sur le forum MSDN. - mais qui ne reçoit pas beaucoup de trafic, pour autant que je peux voir)

J'ai essayé de donner un exemple de Assert et 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;
}

(L'entreprise d'être en mesure de passer dans une référence null au lieu d'une référence Random existant est purement pédagogique, bien sûr.)

Je l'avais espéré que si le vérificateur savait que firstRoll et secondRoll étaient chacun dans la gamme [1, 6], il serait en mesure de travailler que la somme était dans la gamme [2, 12].

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

Si cela est pas pris en charge maintenant, personne ne sait ici si elle est susceptible d'être pris en charge dans un avenir proche-ish?

EDIT: J'ai maintenant trouvé qu'il ya des options très compliquées pour l'arithmétique dans le vérificateur statique. Utilisation de la zone de texte « avancé » je peux les essayer de Visual Studio, mais il n'y a pas d'explication décente de ce qu'ils font, pour autant que je peux dire.

Answer 1

J'ai eu une réponse sur le forum MSDN. Il se trouve que j'étais presque là. Fondamentalement, le vérificateur statique fonctionne mieux si vous divisez des contrats « et ed ». Donc, si nous changeons le code à 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 aussi que l'exemple est encore plus utile, car il met en évidence le point même que le vérificateur fait fonctionnent mieux avec des contrats séparés.

Answer 2

Je ne sais pas sur le MS Contrats outil de vérification, mais l'analyse de gamme est une technique d'analyse standard statique; il est largement utilisé dans les outils d'analyse statique commerciaux pour vérifier que les expressions sont légales en indice.

MS La recherche a un bon bilan à ce type d'analyse statique, et je voudrais donc attendre de faire une telle analyse de portée est un objectif des contrats Checker, même pas actuellement vérifié si.