Code Contracts: IEnumerator<T>.GetEnumerator() weird inherited contract?

Question

I am using Code Contracts together with the Code Contracts Editor Extensions VS2010 add-in. I have a class that implements the IEnumerable<T> interface, and I've implemented an iterator block for the GetEnumerator() method. Above it, I can see the following inherited contract:

I understand the first and third contract requirement - GetEnumerator() must never return a null, and it must never cause a side-effect. But what does the second contract requirement mean? What is this Model property of IEnumerator<T> and of IEnumerable?

EDIT: As Damien_The_Unbeliever pointed out in his comment, the contract for IEnumerable<T> and IEnumerator<T> are located in a seperate file, a Contracts Reference Assembly. Using Reflector, in the disassembly of the contract of those two interfaces (the full code is here), you can see the following:

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

Interestingly, there's an additional contract in GetEnumerator() that isn't displayed by the editor extention:

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

And some additionaly mysteries (such as the Fresh, Escapes and GlobalAccess attributes).

Answer 1

Having taken a second look at the code/contracts loaded from C:\Program Files\Microsoft\Contracts\Contracts.NETFramework\v4.0\mscorlib.Contracts.dll (as referenced in my comment).

I believe it can be safely ignored for your implementation. What it seems to relate to is that it's trying to define a contract such that (effectively) once you're iterating with your IEnumerator object, it will return a certain number of elements. These elements are effectively "snapshotted" when the call to GetEnumerator has returned, and calls to Reset and MoveNext can only iterate over the same set of elements.

I think it's trying to give some immutability guarantees. I've no idea if we can write these same kind of contracts ourselves - it uses the ContractModel attribute, which doesn't seem to be documented anywhere, so far as I can find.

---

Concerning immutablility, etc:

I was mostly looking at the contract for MoveNext on the returned IEnumerator object - basically, it's saying that MoveNext can't change the Model property (that we know was the same Model assigned to it by GetEnumerator), and that the CurrentIndex property is varied between 0 and Model.Length. After that it's just gut feeling/guesswork. I can't point to anything else in the contract assembly that gives me any more info.