Bug in iterators with code contracts?

Question

The following code fails on the pre condition. Is this a bug in code contracts?

static class Program
{
    static void Main()
    {
        foreach (var s in Test(3))
        {
            Console.WriteLine(s);
        }
    }

    static IEnumerable<int>Test (int i)
    {
        Contract.Requires(i > 0);
        for (int j = 0; j < i; j++)
            yield return j;
    }
}

Answer 1

My guess is this has to do with the delayed nature of iterators. Remember, contract processing will occur on the final emitted IL, not the C# code. This means you have to consider the generated code for features like iterators and lambda expressions.

If you decompile that code you'll find that "i" is not actually a parameter. It will be a variable in the class which is used to implement the iterator. So the code actually looks more like the following

class IteratorImpl {
  private int i;
  public bool MoveNext() {
    Contract.Require(i >0);
    ..
  }
}

I'm not terribly familiar with the contract API but my guess is the generated code is much harder to verify.