Code Contracts and type conversion

Question

Hello. I've tried to embrace Microsoft DevLabs Code Contracts static analyzer and faced situation when I do not actually know is it me or is it them. So here is the code:

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

Static analyzer insists that commented post-condition and assert could not be proven. I could not see when it could be wrong.

Edit Even if I replace asserts by assumes post-condition is still unproven.

Answer 1

I tried your example and tried to boil it down to the most basic example.

It seems that there might be a few problems but here is an example that I think may illustrate one major problem:

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

Without code contract specification on called methods the static checker/analyser doesn't seem to be able to work anything else out. The MethodReturningDouble() returns a constant and the static checker doesn't manage to work out that the assert will always pass.

In conclusion, it appears that the static analyser is ONLY for code contracts specifications and not for general analysis.

It is possible to add assumptions about methods you call (that don't have contracts defined):

For example:

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

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

This is a legitimate thing to do if you know for certain that a particular method behaves in a particular way.

Answer 2

Ok, I thought initially I could break it into two parts but realised that my first answer doesn't actually answer the real problem.

Here is the shortest version of your problem:

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

As mentioned by another commenter if you change the hard coded 1.0 to a value <= 0.5 then it passes the check. If it is > 0.5 then it fails.

However if you remove the Contract.Requires(min < max) line then it ALWAYS fails.

I don't have an explanation for this at the moment, sorry.