모듈러스 (%) 연산자에 대한 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) 
     { 
     } 
    } 
} 

그것은 하나 불평하지 않습니다.