コード契約：IEnumerator <T> .GetEnumerator（）weirdは契約を継承していますか？

Question

Code ContractsとCode Contracts Editor Extensions VS2010アドインを使用しています。私はIEnumerable<T>インターフェイスを実装するクラスを持っており、GetEnumerator()メソッドのイテレータブロックを実装しました。 GetEnumerator()がnullを返してはいけません、それは副作用を引き起こすことはありませんしなければならない -

は、私が第一及び第三の契約要件を理解して：その上、私は次の継承された契約書を見ることができます。しかし、2番目の契約要件は何を意味していますか？この Modelのプロパティは IEnumerator<T>と IEnumerableですか？

EDIT：Damien_The_Unbelieverは彼のコメントで指摘したように、IEnumerable<T>とIEnumerator<T>のための契約は別々のファイル、契約リファレンスアセンブリに配置されています。エディタで表示されていないGetEnumerator()に追加の契約があります、興味深いことに

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

：（フルコードはhereである）これらの二つのインターフェースの契約の解体で、Reflectorを使用して、以下を参照してくださいすることができます拡張子：

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

と（例えばFresh、EscapesとGlobalAccess属性など）いくつかのadditionaly謎。

Answer 1

C：\ Program Files \ Microsoft \ Contracts \ Contracts.NETFramework \ v4.0 \ mscorlib.Contracts.dllからロードされたコード/コントラクトをもう一度見てきました。

あなたの実装では無視しても問題ないと思います。これは、あなたがIEnumeratorオブジェクトを反復すると（効果的に）一定の数の要素を返すような契約を定義しようとしていることです。これらの要素は、GetEnumeratorの呼び出しが返され、ResetおよびMoveNextの呼び出しが同じ要素のセットに対してのみ反復処理できる場合、効果的に「スナップショット」されます。

私はそれがいくつかの不変性を保証しようとしていると思います。私たちは、同じ種類の契約書を自分たちで書くことができないのかどうかはわかりません。ContractModel属性を使用しています。これはどこにも書かれていないようです。

immutablilityなどに関する

---

：私は主に返されるのIEnumeratorオブジェクトのMoveNextメソッドのための契約を見ていた

を - 基本的に、我々がした知っていること（MoveNextメソッドは、モデルのプロパティを変更することはできませんと言っていますGetEnumeratorによって割り当てられた同じモデル）、CurrentIndexプロパティは0とModel.Lengthの間で変更されます。それはちょうど直感/推測です。私は何も情報を与えない契約組合の何かを指すことはできません。