Contratos de código: IEnumerator <T> .GetEnumerator() raro contrato heredado?

Question

Estoy usando Code Contracts junto con el complemento Code Contracts Editor Extensions VS2010. Tengo una clase que implementa la interfaz IEnumerable<T>, y he implementado un bloque iterador para el método GetEnumerator(). Por encima de él, puedo ver el siguiente contrato heredado:

entiendo el primer y tercer requisito contrato - GetEnumerator() nunca debe devolver un valor nulo, y nunca deben causar un efecto secundario. ¿Pero qué significa el segundo requisito de contrato? ¿Qué es esto Model propiedad de IEnumerator<T> y de IEnumerable?

EDIT: Como Damien_The_Unbeliever señaló en su comentario, el contrato para IEnumerable<T> y IEnumerator<T> se encuentran en un archivo separado, un conjunto de referencia contratos. Usando Reflector, en el desmontaje del contrato de esas dos interfaces (el código completo es here), se puede ver lo siguiente:

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

Curiosamente, hay un contrato adicional en GetEnumerator() que no se visualiza por el editor extensión:

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

y algunos misterios adicionados (tales como los Fresh, EscapesGlobalAccess y atributos).

Answer 1

Después de echar un segundo vistazo al código/contratos cargados desde C: \ Archivos de programa \ Microsoft \ Contracts \ Contracts.NETFramework \ v4.0 \ mscorlib.Contracts.dll (como se hace referencia en mi comentario).

Creo que se puede ignorar con seguridad para su implementación. Lo que parece relacionarse es que está tratando de definir un contrato tal que (efectivamente) una vez que está iterando con su objeto IEnumerator, devolverá una cierta cantidad de elementos. Estos elementos se "capturan" de forma efectiva cuando la llamada a GetEnumerator ha regresado, y las llamadas a Reset y MoveNext solo pueden iterar sobre el mismo conjunto de elementos.

Creo que está tratando de dar algunas garantías de inmutabilidad. No tengo idea de si podemos escribir estos mismos tipos de contratos: utiliza el atributo ContractModel, que no parece estar documentado en ningún lugar, hasta donde puedo encontrar.

---

immutablility En cuanto, etc:

que estaba buscando su mayor parte en el contrato para MoveNext en el objeto IEnumerator regresado - Básicamente, es decir que MoveNext no puede cambiar la propiedad de modelo (que sabemos que fue el mismo modelo asignado por GetEnumerator), y que la propiedad CurrentIndex se varía entre 0 y Model.Length. Después de eso es solo una corazonada/conjetura. No puedo señalar nada más en el ensamblaje del contrato que me da más información.