代码契约中的迭代器存在 Bug 吗？

Question

以下代码未能满足前置条件。这是代码合约中的一个错误吗？

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

- pn.

Answer 1

我猜这与迭代器的延迟性有关。请记住，合同处理将在最终发出的IL上进行，而不是C#代码上进行。这意味着您必须考虑生成的代码中是否存在迭代器和lambda表达式等功能。

如果您反编译该代码，您会发现“i”实际上不是一个参数。它将是一个用于实现迭代器的类中的变量。因此，代码实际上看起来更像以下内容：

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

我对合约API并不是很熟悉，但我猜生成的代码可能更难以验证。

- JaredPar

---

为什么Requires应该在IteratorImpl的MoveNext而不是构造函数中？ - pn.

@pn，这只是C#团队选择实现迭代器的方式。任何出现在迭代器主体中的代码都将最终出现在生成代码的MoveNext方法中。 - JaredPar

我的问题是这是否是代码合同中的一个错误。看起来代码合同重写器不理解迭代器。 - pn.

@pn，我觉得问题在于作者不理解迭代器对代码约束的影响。 - JaredPar

Answer 2

记住，迭代器在枚举之前不会运行，并且会在后端编译成一些特殊的代码。如果您想要验证参数，这通常也适用于合同，请遵循以下一般模式：使用包装函数：

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

这样，当调用Test()时，它将检查参数，然后返回_Test()，实际上只是返回一个新类。

- Talljoe

---

这是一种解决方法。但是，我应该改变我的代码还是这是一个将被修复的错误？ - pn.

这就是迭代器的工作方式 - C# 不会改变这种行为。如果您需要检查方法的参数，并希望在调用时而不是在枚举时执行此操作，则必须将其包装在第二个执行检查的方法中。我不知道合同是否会自我修复以更好地与迭代器配合使用。 - Talljoe

Answer 3

这可能过去在 CodeContract 重写器中存在问题。但是当前版本似乎对您的示例运行良好。迭代器/延迟评估等方面没有任何问题。参数 i 被按值捕获，不会在迭代期间更改。合同应仅在调用 Test 的开始时检查此问题，而不是在每次迭代期间检查。

- Manuel Fahndrich

Answer 4

这段代码将与.NET 4.0的最终版本（我刚试过）一起工作，其中支持迭代器中的代码合同，但正如我最近发现的那样，它并不总是正常工作的（在这里阅读更多信息）。

- Jarek Kardas

Answer 5

这里有一篇博客文章，与单元测试、迭代器、延迟执行以及你有关。

问题在于延迟执行。

- jason