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

【问题标题】：CodeContracts on modulus (%) operator fail?模数 (%) 运算符的 CodeContracts 失败？
【发布时间】：2012-01-05 16:12:14
【问题描述】：

我正在编写一个专门的随机生成器类，并希望使用 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 在最后一个“确保”时会失败？

【问题讨论】：

可能是因为maxValue != max.
如果max==0 您的代码抛出异常。您的 max 参数的命名也很糟糕，因为它不代表最大值，而是最大值加一。
您的代码甚至无法编译。你有一个max 和一个maxValue。
maxValue 是全局变量吗？
@KevinCrowell 即使它是int 类型的全局变量，代码合同也不会抱怨。

标签： c# .net random code-contracts modulus

【解决方案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 替换它，它也不会抱怨。

【讨论】：