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