2

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?

John Gietzen
  • 48,783
  • 32
  • 145
  • 190

2 Answers2

3

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?

Jon Skeet
  • 1,421,763
  • 867
  • 9,128
  • 9,194
  • Yes, I checked that this simplified version does exactly that. I this it is a bug in the static checker. In this case, I *could* use enumeration, but to me, the "right way" seems to be to access by index (since I am accessing it in an ordered fashion.) – John Gietzen Aug 05 '09 at 14:03
  • `foreach` is ordered when you access it on a naturally ordered collection though (like a list). You only need to worry about ordering failing for things like sets. However, that's beside the point. What happens if you uncomment each of the commented lines? – Jon Skeet Aug 05 '09 at 14:32
  • Neither has an effect. Which is precisely why I thought it may be a bug. – John Gietzen Aug 05 '09 at 14:54
1

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.

hwiechers
  • 14,583
  • 8
  • 53
  • 62