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