我尝试使用 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;
}
静态分析器坚持认为无法证明评论后的条件和断言。我看不出它什么时候会出错。
编辑即使我用假设后置条件替换断言仍然未经证实。