[ContractClassFor(typeof(IEnumerable))]
internal abstract class IEnumerableContract : IEnumerable
{
// Methods
protected IEnumerableContract()
{
}
[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;
}
// Properties
public object[] Model
{
get
{
object[] objArray;
Contract.Ensures((bool)(Contract.Result<object[]>() != null), null, "Contract.Result<object[]>() != null");
return objArray;
}
}
}
[ContractClassFor(typeof(IEnumerator))]
internal abstract class IEnumeratorContract : IEnumerator
{
// Methods
protected IEnumeratorContract() { }
public bool MoveNext()
{
bool flag;
Contract.Ensures((bool)(this.Model == Contract.OldValue<object[]>(this.Model)), null, "this.Model == Contract.OldValue(this.Model)");
Contract.Ensures((bool)(this.CurrentIndex < this.Model.Length), null, "this.CurrentIndex < this.Model.Length");
Contract.Ensures((bool)(this.CurrentIndex >= 0), null, "this.CurrentIndex >= 0");
Contract.Ensures((bool)(this.CurrentIndex == (Contract.OldValue<int>(this.CurrentIndex) + 1)), null, "this.CurrentIndex == Contract.OldValue(this.CurrentIndex) + 1");
return flag;
}
public void Reset() { }
// Properties
public object Current
{
get
{
object obj2;
Contract.Ensures((bool)(Contract.Result<object>() == this.Model[this.CurrentIndex]), null, "Contract.Result<object>() == this.Model[this.CurrentIndex]");
return obj2;
}
}
public int CurrentIndex
{
get
{
int num;
return num;
}
}
public object[] Model
{
get
{
object[] objArray;
return objArray;
}
}
}