CODEWITHSUNDEEP
c#.net.net-4.0code-contractsmicrosoft-contracts
pn.
pn.

Reputation: 872

Bug in iterators with code contracts?

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;
    }
}

Upvotes: 7

Views: 417

Answers (5)

Manuel Fahndrich
Manuel Fahndrich

Reputation: 665

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.

Upvotes: 0

Jarek Kardas
Jarek Kardas

Reputation: 8455

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).

Upvotes: 0

jason
jason

Reputation: 241779

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

Delayed execution is the issue here.

Upvotes: 0

Talljoe
Talljoe

Reputation: 14827

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.

Upvotes: 0

JaredPar
JaredPar

Reputation: 755397

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.

Upvotes: 2

Related Questions