Code Contracts and Type Conversion

Question

I tried to use Microsoft DevLabs Code Contracts Static Component Analyzer and came across a situation where I really don't know if it is me or these. 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; } 

The static analyzer insists that commented postconditions and statements cannot be proved. I could not understand when this might be wrong.

Edit Even if I replace the statements, suppose that the post-condition is still unproven.

Answer 1

Well, I thought that at first I could break it into two parts, but I realized that my first answer did not really 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 commentator, if you change hard-coded 1.0 to <= 0.5, then it will pass the test. If it is> 0.5, then it fails.

However, if you delete the line Contract.Requires (min <max), then it will ALWAYS fail.

I have no explanation for this at the moment, sorry.

Answer 2

I tried your example and tried to weld it to the most elementary example.

It seems that there may be several problems, but here is an example that, I think, can illustrate one serious 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 the specification of the code contract for the called methods, the static controller / analyzer does not seem to be able to work in any other way. MethodReturningDouble () returns a constant, and the static controller cannot decide that the statement will always pass.

In conclusion, it turns out that the static analyzer is ONLY for code contract specifications, and not for general analysis.

You can add assumptions about the methods you call (which do not have specific contracts):

For instance:

 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 if you know for sure that a particular method behaves in a certain way.