c# - 模数 (%) 运算符的 CodeContracts 失败？

Question

我正在编写一个专门的随机器类，并希望使用 CodeContracts 确保它的质量。典型的随机化器方法接收上限“最大值”并返回低于该限制的正随机值。

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

wherepick()返回一个随机数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.