模数 (%) 运算符上的 CodeContracts 失败？

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 类型的单独变量而不是用 替换它，它也不会抱怨>最大。