代码合同和类型转换

Question

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

静态分析器坚持认为被注释的后置条件和断言无法证明。我无法看出它何时可能是错误的。

编辑 即使我用假设替换断言，后置条件仍然无法证明。

- Artem Tikhomirov

---

已经有一个 System.Random.Next(int min, int max) 方法了。但是 max 参数是一个排除的上限。 - Wim Coenen

谢谢。我只是为了方便插入了 System.Random.Next() 调用。我在那个地方使用了加密强的随机算法，但问题无论如何都会出现。 - Artem Tikhomirov

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更改为小于等于0.5的值，则它会通过检查。如果大于0.5，则不会通过。

但是，如果您删除Contract.Requires（min <max）行，则始终会失败。

目前我没有解释，请见谅。

- Matt Breckon

---

感谢Matt的研究。我得出了相同的结论。静态检查器中有些问题，现在我非常确定这是正确的，因为你独立得出了这个结论。我现在会为那个文件打开静态验证。 - Artem Tikhomirov

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

这是一个合理的做法，如果你确定某个方法会以特定的方式运行。

- Matt Breckon

---

从代码合同页面“cccheck，一种静态检查器，可以在编译时验证合同。” - 这似乎支持结论，即验证器仅用于验证合同。 - Matt Breckon

除非我弄错了，Artem已经尝试将Assert改为Assume。如果没有尝试过，我已经尝试过并且这并没有起作用。如果您将basicRandom变量硬编码为任何<=0.5的值，则检查器将通过该例程（在进行假设更改后）。 将其更改为任何> 0.5的值（例如0.5000001），则无法验证它。 这使我认为这里有更微妙的问题，我看不到。 不管怎样，我很想找出发生了什么！ - FinnNk

是的，我刚刚意识到了这一点。我添加了另一个答案，以最简形式呈现问题。 - Matt Breckon

好的，这很奇怪 - 我的更新版本没有表现出小于0.5和大于0.5的问题。我会重新检查我的假设。 - Matt Breckon