代码契约和类型转换

Question

我尝试使用 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;
    }

静态分析器坚持认为无法证明已评论的后置条件和断言。我看不出什么时候会出错。

编辑即使我将断言替换为假设后置条件仍然未经证实。

Answer 1

好的，我最初以为我可以将它分成两部分，但意识到我的第一个答案实际上并没有回答真正的问题。

这是您问题的最短版本：

    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 更改为值

但是，如果您删除 Contract.Requires(min

抱歉，目前我对此没有任何解释。

Answer 2

我尝试了您的示例并尝试将其归结为最基本的示例。

似乎可能存在一些问题，但我认为这里有一个例子可以说明一个主要问题：

public static void TestMethod()
{
    double d = MethodReturningDouble();
    Contract.Assert(d >= 0.0);
    Contract.Assert(d <= 4.0);
}

public static double MethodReturningDouble()
{
  //  Contract.Ensures(Contract.Result<double>() <= 4.0); // <- without this line the above asserts are unproven
    return 3.0;
}

如果没有调用方法的代码契约规范，静态检查器/分析器似乎无法解决任何其他问题。 MethodReturningDouble() 返回一个常量，静态检查器无法确定断言将始终通过。

总之，静态分析器似乎仅用于代码合约规范，而不用于一般分析。

可以添加关于您调用的方法的假设（没有定义合同）：

例如：

public static void TestMethodUsingRandom()
{
    double d = new Random().NextDouble();
    Contract.Assume(d <= 1.0);

    Contract.Assert(d >= 0.0);
    Contract.Assert(d <= 4.0);
}

如果您确定特定方法以特定方式运行，则这样做是合法的。