Should the Code Contracts static checker be able to check arithmetic bound?

I’ve had an answer on the MSDN forum. It turns out I was very nearly there. Basically the static checker works better if you split out “and-ed” contracts. So, if we change the code to this: public static int RollDice(Random rng) { Contract.Ensures(Contract.Result<int>() >= 2); Contract.Ensures(Contract.Result<int>() <= 12); if (rng == null) { rng = … Read more