What does it take to prove this Contract.Requires?

Question

I have an application that runs through the rounds in a tournament, and I am getting a contract warning on this simplified code structure:

    public static void LoadState(IList<Object> stuff)
    {
        for(int i = 0; i < stuff.Count; i++)
        {
            // Contract.Assert(i < stuff.Count);
            // Contract.Assume(i < stuff.Count);

            Object thing = stuff[i];

            Console.WriteLine(thing.ToString());
        }
    }

The warning is:

contracts: requires unproven: index < @this.Count

What am I doing wrong? How can I prove this on an IList<T>? Is this a bug in the static analyzer? How would I submit a bug report to Microsoft?

Answer 1

That does look odd. Unfortunately I'm using the Pro version of VS2010 with Code Contracts, so I can't run cccheck myself to play around.

Do you definitely need the index rather than just using a foreach loop?

Just to be sure - does your simplified example above produce the same error? It's always worth checking that the simplification hasn't removed the problem :) For instance, do you do anything else to stuff which the contract checker might use to invalidate the guarantee about stuff.Count?

Answer 2

I checked this with version 1.2.21023.14 of code contracts and didn't get warnings. My guess is that it is a bug that has since been fixed.