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.

Answer 2

Remember that iterators aren't run until they are enumerated, and are compiled into some special sauce in the back end. The general pattern you should follow if you want to validate parameters, and this probably holds true for contracts, is to have a wrapper function:

static IEnumerable<int> Test (int i)
{
    Contract.Requires(i > 0);
    return _Test(i);
}

private static IEnumerable<int> _Test (int i)
{
    for (int j = 0; j < i; j++)
        yield return j;
}

That way Test() will do the checking of the parameters when it is called then return _Test(), which actually just returns a new class.

Answer 3

Here's a blog post related to this very subject concerning unit testing, iterators, delayed execution, and you.

Delayed execution is the issue here.

Answer 4

This code will work with final version of .NET 4.0 (just tried it) where Code Contracts in interators are supported, but as I found out recently it does not always work properly (read more here).

Answer 5

This may have been a problem in the CodeContract rewriter in the past. But the current version seems to do fine on your example. There's no issue here with iterators/delayed evaluation etc. The parameter i is captured by value and won't change during the iteration. Contracts should check this only at the beginning of the call to Test, not during each iteration.