代码合同和类型转换

我试图接受微软DevLabs代码合同静态分析器，并遇到了当我实际上不知道它是我还是他们时的情况。所以这是代码：代码合同和类型转换

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

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

编辑即使我假设后置条件仍未被证实。

来源

2009-10-31 Artem Tikhomirov

已经有一个'System.Random.Next（int min，int max）'方法。但最大参数是唯一的上限。 – 2009-10-31 12:06:43

谢谢。为了方便，我插入了System.Random.Next（）调用。我使用的是密码强度随机算法，但问题以任何方式发生。 – 2009-11-01 13:04:55

我试过你的例子，并试图将其归结为最基本的例子。

看来，可能有一些问题，但这里是我认为可以说明一个重大问题的例子：如果没有代码合同规范上调用的方法静态检测/分析仪似乎并不

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

这是，如果你肯定知道做合法的事一个特定的方法以特定的方式表现。

来源

2009-10-31 13:08:35

从代码合同页面“cccheck，一个在编译时验证合同的静态检查器” - 这似乎支持验证器只用于验证合同的结论。 http://research.microsoft.com/en-us/projects/contracts/ – 2009-10-31 13:17:45

除非我错了Artem已经尝试将Assert改为Assume。如果没有，我有，这并不能解决问题。如果将basicRandom变量更改为硬编码为<= 0的任何值。5检查员将通过例程（假定改变之后）。将其更改为大于0.5（例如0.5000001），并且无法验证它。这让我觉得在这里我看不到一些更微妙的东西。无论如何，我很想知道发生了什么！ – FinnNk 2009-10-31 14:21:23

是的，我刚才意识到这一点。我添加了另一个以最小的形式呈现问题的答案。 – 2009-10-31 14:47:02

好吧，我想最初我可以把它分成两部分，但意识到我的第一个答案并不真正回答真正的问题。

这是你的问题的最短版本：

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（最小< max）行，那么它总是失败。

我现在没有对此的解释，对不起。

来源

2009-10-31 14:45:59

谢谢你的研究马特。我已经走到了同一个目标。有些事情在静态检查器的那个部分是错误的，现在我非常肯定它是这种情况，因为你已经独立地得出了这个结论。我现在将打开该文件的静态验证。 – 2009-11-01 13:11:45

代码合同和类型转换

回答

相关问题