モジュラス（％）演算子のCodeContractsが失敗しますか？

Question

私は特別なランダマイザクラスを作成しており、CodeContractsを使用してその品質を保証したいと考えています。典型的なランダム化方法は上限値「max」を受け取り、その限界値以下の正のランダム値を返す。 pick()がランダムUInt32返し

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

。私の質問：CodeContractsが最後の "保証"に失敗するのはなぜですか？

Answer 1

問題を再現できません。コードの契約は、次のコード文句はありません：私はmaxでそれを置き換えるのではなく、タイプintの別々の変数としてごmaxValueを続ければ

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) 
     { 
     } 
    } 
} 

それはどちらか文句はありません。