Is the Random.Next code contract incorrect?

I've installed a plugin (Code Contract Editor Extensions by Micro开发者_Go百科soft) which displays all code contracts for .NET.

When I look at the contract for Random.Next it says ensures result <= maxValue while MSDN states that maxValue is exclusive. Shouldn't the contract say ensures result < maxValue?

It is not exclusive, and MSDN does not state that it is. Well, OK, it does use the word "exclusive" when talking about maxValue, which is less than clear, but the reality is that in the vast majority of cases it is indeed exclusive as expected.

There are, however, some corner-cases: to be specific with examples, Next(0) returns 0; Next(4,4) returns 4. It is inclusive when it has no option, and this is documented in the "Return Value" sections on MSDN:

To quote from Next(maxValue):

However, if maxValue equals zero, maxValue is returned.

and from Next(minValue,maxValue):

If minValue equals maxValue, minValue is returned.

(which of course could also be stated "maxValue is returned")

So in both cases, it is possible for maxValue to be returned.

The only exception is the parameterless Next() which is documented as being strictly < int.MaxValue.

Since the contract in MSDN is stricter than the contract used by code contracts, the contract used by code contracts is obviously correct, but perhaps not tight.

On the other hand if you were to supply a custom implementation of Next in your own Random derived class, it might not fulfill the contract specified on MSDN, but the contract checker won't notice the mistake. So it's still advisable for MS to remove the discrepancy between the two contract versions.

I wouldn't be surprised if the MSDN behavior was originally a mistake and they then changed the code to fit the specification.

I suggest that you file a MS Connect issue asking them to improve one of them.

Quoting MSDN for Next()

A 32-bit signed integer greater than or equal to zero and less than MaxValue.