c# – 代码合同和类型转换

我试图接受Microsoft DevLabs Code Contracts静态分析器并面对我实际上不知道是我还是它们的情况.所以这是代码：

    public static int GenerateInBetween(int min, int max)
    {
        Contract.Requires(min < max);
        Contract.Requires((long)(max - min) <= (long)(Int32.MaxValue));

        Contract.Ensures(Contract.Result<int>() >= min);
        Contract.Ensures(Contract.Result<int>() <= max);  // Unpvoven!

        long range = max - min;

        double basicRandom = new Random().NextDouble();
        Contract.Assert(basicRandom >= 0.0);
        Contract.Assert(basicRandom <= 1.0);              // Unpvoven!

        double randomDouble = basicRandom * range;
        Contract.Assert(randomDouble >= 0.0);
        Contract.Assert(randomDouble <= (double)range);   // Unpvoven!

        int randomInt32 = (int)randomDouble;
        Contract.Assert(randomInt32 >= 0);
        Contract.Assert(randomInt32 <= range);

        return min + randomInt32;
    }

静态分析器坚持认为无法证明评论后的条件和断言.我看不出什么时候可能是错的.

编辑即使我通过假设后置条件替换断言仍然未经证实.

解决方法:

好吧,我想我最初可以把它分成两部分但是我意识到我的第一个答案实际上并没有回答真正的问题.

这是您问题的最短版本：

    public static void GenerateInBetween(double min, double max)
    {
        Contract.Requires(min < max);
        double range =  max - min;

        double randomDouble = 1.0 * range;
        Contract.Assert(randomDouble <= range);   
    }

正如另一位评论者所提到的,如果您将硬编码1.0更改为值<= 0.5,则它会通过检查.如果是> 0.5然后它失败了. 但是,如果删除Contract.Requires(min< max)行,则它始终失败. 对不起,我暂时没有这方面的解释.

标签：c,net,code-contracts
来源： https://codeday.me/bug/20190710/1423503.html