CodeContracts по оператору модуля (%) не удалось? - PullRequest
Новая
       24

CodeContracts по оператору модуля (%) не удалось?

0 голосов
/ 05 января 2012

Я пишу специализированный класс рандомизаторов и хочу гарантировать его качество с помощью CodeContracts. Типичный метод рандомизатора получает верхний предел 'max' и возвращает положительное случайное значение ниже этого предела. 

public int Next(int max)
{
    Contract.Requires<ArgumentOutOfRangeException>(0 <= max && max <= int.MaxValue);
    Contract.Ensures(0 <= Contract.Result<int>());
    Contract.Ensures(Contract.Result<int>() < maxValue);

    return (int)(pick() % maxValue);
}

, где pick() возвращает случайное UInt32. Мой вопрос: почему CodeContracts терпит неудачу при последнем "обеспечении"?

1 Ответ

2 голосов
/ 06 января 2012

Я не могу воспроизвести вашу проблему.Контрактный код не жалуется на следующий код: 

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;

namespace ContractModulo
{
    class Program
    {
        UInt32 Pick()
        {
            return 0;
        }

        public int Next(int max)
        {
            Contract.Requires<ArgumentOutOfRangeException>(0 <= max && max <= int.MaxValue);
            Contract.Ensures(0 <= Contract.Result<int>());
            Contract.Ensures(Contract.Result<int>() < max);

            return (int)(Pick() % max);
        }

        static void Main(string[] args)
        {
        }
    }
}

Также не будет жаловаться, если я сохраню вашу maxValue как отдельную переменную типа int вместо ее замены на max.

...