-1

私は特殊なランダマイザー クラスを作成しており、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);
}

wherepick()は random を返しますUInt32。私の質問: 最後の「保証」で CodeContracts が失敗するのはなぜですか?

4

1 に答える 1

2

問題を再現できません。コード コントラクトは、次のコードについて文句を言いません。

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

your をに置き換えるのではなく、maxValueタイプの別の変数として保持しても文句はありません。intmax

于 2012-01-05T20:13:26.113 に答える