代码契约:IEnumerator <T> .GetEnumerator()奇怪的继承契约？

Question

我正在使用Code Contracts和Code Contracts Editor Extensions VS2010加载项.我有一个实现IEnumerable<T>接口的类,我已经为该GetEnumerator()方法实现了一个迭代器块.在它上面,我可以看到以下继承的合同:

我理解第一个和第三个合同要求 - GetEnumerator()必须永远不会返回null,并且它必须永远不会导致副作用.但第二份合同要求意味着什么？这个Model属性IEnumerator<T>是IEnumerable什么？

编辑:正如Damien_The_Unbeliever在他的评论中所指出的那样,合同IEnumerable<T>和IEnumerator<T>位于一个单独的文件,一个合同参考大会.使用Reflector,在这两个接口的合同的反汇编中(完整代码在这里),您可以看到以下内容:

[return: Fresh]
[Escapes(true, false), Pure, GlobalAccess(false)]
public IEnumerator GetEnumerator()
{
    IEnumerator enumerator;
    Contract.Ensures((bool) (Contract.Result<IEnumerator>() != null), null, "Contract.Result<IEnumerator>() != null");
    Contract.Ensures((bool) (Contract.Result<IEnumerator>().Model == this.Model), null, "Contract.Result<IEnumerator>().Model == this.Model");
    Contract.Ensures((bool) (Contract.Result<IEnumerator>().CurrentIndex == -1), null, "Contract.Result<IEnumerator>().CurrentIndex == -1");
    return enumerator;
}

有趣的是,GetEnumerator()编辑器扩展中没有显示额外的合同:

Contract.Result<IEnumerator>().CurrentIndex == -1

而一些additionaly奥秘(如Fresh,Escapes和GlobalAccess属性).

Answer 1

再次查看从 C:\Program Files\Microsoft\Contracts\Contracts.NETFramework\v4.0\mscorlib.Contracts.dll 加载的代码/合同（如我的评论中所引用）。

我相信在您的实施中可以安全地忽略它。它似乎涉及的是，它试图定义一个契约，以便（有效地）一旦你迭代你的IEnumerator对象，它将返回一定数量的元素。当对 GetEnumerator 的调用返回时，这些元素实际上被“快照”，并且对 Reset 和 MoveNext 的调用只能迭代同一组元素。

我认为它试图提供一些不变性保证。我不知道我们是否可以自己编写这些相同类型的合约 - 它使用该ContractModel属性，据我所知，该属性似乎没有在任何地方记录。

关于不变性等：

我主要查看返回的 IEnumerator 对象上的 MoveNext 契约 - 基本上，它表示 MoveNext 无法更改 Model 属性（我们知道与 GetEnumerator 分配给它的模型相同），并且 CurrentIndex 属性是变化的介于 0 和 Model.Length 之间。之后，这只是直觉/猜测。我无法指出合同汇编中的任何其他内容可以为我提供更多信息。