코드 계약 : IEnumerator <T> .GetEnumerator() weird 상속 된 계약?

Question

Code Contracts을 Code Contracts Editor Extensions VS2010 추가 기능과 함께 사용하고 있습니다. IEnumerable<T> 인터페이스를 구현하는 클래스가 있고 GetEnumerator() 메서드에 대한 반복기 블록을 구현했습니다. GetEnumerator()가 널을 반환해서는 안, 그리고 부작용을 야기해서는 안 -

나는 첫 번째와 세 번째 계약 요구 사항을 이해 : 그것보다도, 나는 다음과 같은 상속 된 계약을 볼 수 있습니다. 그러나 두 번째 계약 요구 사항은 무엇을 의미합니까? Model 속성은 IEnumerator<T>이고 IEnumerable은 무엇입니까?

편집 : 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 사이에서 변경됩니다. 그 후에 그것은 단지 직감/추측입니다. 나에게 더 많은 정보를주는 계약 어셈블리의 다른 것을 지적 할 수는 없다.