Contratti di codice: IEnumerator <T> .GetEnumerator() contratto ereditato strano?

Question

Sto utilizzando Code Contracts insieme al componente aggiuntivo Code Contracts Editor Extensions VS2010. Ho una classe che implementa l'interfaccia IEnumerable<T> e ho implementato un blocco iteratore per il metodo GetEnumerator(). Sopra di esso, posso vedere il seguente contratto ereditato:

Capisco il primo e il terzo requisito contratto - GetEnumerator() deve mai restituire un nulla, e non deve mai causare un effetto collaterale. Ma cosa significa il secondo requisito del contratto? Che cos'è questa proprietà Model di IEnumerator<T> e di IEnumerable?

EDIT: Come Damien_The_Unbeliever ha sottolineato nel suo commento, il contratto per IEnumerable<T> e IEnumerator<T> si trovano in un file separato, un Contratti Assemblea di riferimento. Utilizzando Reflector, nel disassemblaggio del contratto di questi due interfacce (il codice completo è here), è possibile vedere il seguente:

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

È interessante notare che c'è un contratto aggiuntivo in GetEnumerator() che non viene visualizzato l'editor extention:

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

e alcuni misteri additionaly (come i Fresh, Escapes e GlobalAccess attributi).

Answer 1

Avendo dato una seconda occhiata al codice/contratti caricati da C: \ Programmi \ Microsoft \ Contracts \ Contracts.NETFramework \ v4.0 \ mscorlib.Contracts.dll (come riferito nel mio commento).

Credo che possa essere tranquillamente ignorato per la vostra implementazione. Quello che sembra riguardare è che sta cercando di definire un contratto tale che (efficacemente) una volta che si sta iterando con l'oggetto IEnumerator, restituirà un certo numero di elementi. Questi elementi sono effettivamente "snapshot" quando viene restituita la chiamata a GetEnumerator e le chiamate a Reset e MoveNext possono solo scorrere sullo stesso insieme di elementi.

Penso che stia cercando di dare alcune garanzie di immutabilità. Non ho idea se possiamo scrivere lo stesso tipo di contratti da soli - utilizza l'attributo ContractModel, che non sembra essere documentato da nessuna parte, per quanto posso trovare.

---

Per quanto riguarda immutablility, ecc:

stavo per lo più guardando il contratto per MoveNext sull'oggetto IEnumerator tornato - in fondo, è dire che MoveNext non può cambiare la proprietà del modello (che sappiamo è stato il stesso modello ad esso assegnato da GetEnumerator) e che la proprietà CurrentIndex è variata tra 0 e Model.Length. Dopo di che è solo una sensazione istintiva/congettura. Non riesco a indicare altro nell'assemblea del contratto che mi dia ulteriori informazioni.