Ошибка в кодеКонтракты по модулю (%)?

Question

Я пишу специализированный класс рандомизатора и хочу обеспечить его качество с помощью 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 терпят неудачу при последнем «обеспечении»?

Answer 1

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

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.