Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- [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;
- }
- }
- }
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement