Кодовые контракты и преобразование типов - PullRequest
Новая
       18

Кодовые контракты и преобразование типов

4 голосов
/ 31 октября 2009

Я пытался использовать статический анализатор Microsoft DevLabs Code Contracts и столкнулся с ситуацией, когда я на самом деле не знаю, это я или это они. Итак, вот код: 

    public static int GenerateInBetween(int min, int max)
    {
        Contract.Requires(min < max);
        Contract.Requires((long)(max - min) <= (long)(Int32.MaxValue));

        Contract.Ensures(Contract.Result<int>() >= min);
        Contract.Ensures(Contract.Result<int>() <= max);  // Unpvoven!

        long range = max - min;

        double basicRandom = new Random().NextDouble();
        Contract.Assert(basicRandom >= 0.0);
        Contract.Assert(basicRandom <= 1.0);              // Unpvoven!

        double randomDouble = basicRandom * range;
        Contract.Assert(randomDouble >= 0.0);
        Contract.Assert(randomDouble <= (double)range);   // Unpvoven!

        int randomInt32 = (int)randomDouble;
        Contract.Assert(randomInt32 >= 0);
        Contract.Assert(randomInt32 <= range);

        return min + randomInt32;
    }

Статический анализатор настаивает на том, что прокомментированные постусловия и утверждения не могут быть доказаны. Я не мог понять, когда это могло быть не так.

Редактировать Даже если я заменяю утверждения на предполагается, что постусловие все еще не доказано.

Ответы [ 2 ]

1 голос
/ 31 октября 2009

Хорошо, сначала я думал, что смогу разбить его на две части, но понял, что мой первый ответ на самом деле не отвечает реальной проблеме.

Вот самая короткая версия вашей проблемы: 

    public static void GenerateInBetween(double min, double max)
    {
        Contract.Requires(min < max);
        double range =  max - min;

        double randomDouble = 1.0 * range;
        Contract.Assert(randomDouble <= range);   
    }

Как уже упоминалось другим комментатором, если вы измените жестко запрограммированный 1.0 на значение <= 0.5, то он пройдет проверку. Если это> 0,5, то это не удается.

Однако, если вы удалите строку Contract.Requires (min

У меня нет объяснения этому на данный момент, извините.

0 голосов
/ 31 октября 2009

Я попробовал ваш пример и попытался свести его к самому простому примеру.

Кажется, что может быть несколько проблем, но вот пример, который, я думаю, может проиллюстрировать одну большую проблему: 

public static void TestMethod()
{
    double d = MethodReturningDouble();
    Contract.Assert(d >= 0.0);
    Contract.Assert(d <= 4.0);
}

public static double MethodReturningDouble()
{
  //  Contract.Ensures(Contract.Result<double>() <= 4.0); // <- without this line the above asserts are unproven
    return 3.0;
}

Без спецификации контракта кода для вызываемых методов статическая проверка / анализатор, кажется, не в состоянии решить что-либо еще. MethodReturningDouble () возвращает константу, и статическому контролеру не удается определить, что утверждение всегда будет проходить.

В заключение, кажется, что статический анализатор ТОЛЬКО для спецификаций контрактов кода, а не для общего анализа.

Можно добавить предположения о методах, которые вы вызываете (для которых не определены контракты):

Например: 

public static void TestMethodUsingRandom()
{
    double d = new Random().NextDouble();
    Contract.Assume(d <= 1.0);

    Contract.Assert(d >= 0.0);
    Contract.Assert(d <= 4.0);
}

Это допустимо, если вы точно знаете, что определенный метод ведет себя определенным образом.

...