ContractClassAttribute Class

Imports System
Imports System.Diagnostics.Contracts


' An IArray is an ordered collection of objects.    
<ContractClass(GetType(IArrayContract))> _
Public Interface IArray
    ' The Item property provides methods to read and edit entries in the array.

    Default Property Item(ByVal index As Integer) As [Object]


    ReadOnly Property Count() As Integer


    ' Adds an item to the list.  
    ' The return value is the position the new element was inserted in.
    Function Add(ByVal value As Object) As Integer

    ' Removes all items from the list.
    Sub Clear()

    ' Inserts value into the array at position index.
    ' index must be non-negative and less than or equal to the 
    ' number of elements in the array.  If index equals the number
    ' of items in the array, then value is appended to the end.
    Sub Insert(ByVal index As Integer, ByVal value As [Object])


    ' Removes the item at position index.
    Sub RemoveAt(ByVal index As Integer)
End Interface 'IArray

<ContractClassFor(GetType(IArray))> _
Friend MustInherit Class IArrayContract
    Implements IArray

    Function Add(ByVal value As Object) As Integer Implements IArray.Add
        ' Returns the index in which an item was inserted.
        Contract.Ensures(Contract.Result(Of Integer)() >= -1) '
        Contract.Ensures(Contract.Result(Of Integer)() < CType(Me, IArray).Count) '
        Return 0

    End Function 'IArray.Add

    Default Property Item(ByVal index As Integer) As Object Implements IArray.Item
        Get
            Contract.Requires(index >= 0)
            Contract.Requires(index < CType(Me, IArray).Count)
            Return 0 '
        End Get
        Set(ByVal value As [Object])
            Contract.Requires(index >= 0)
            Contract.Requires(index < CType(Me, IArray).Count)
        End Set
    End Property

    Public ReadOnly Property Count() As Integer Implements VB.IArray.Count
        Get
            Contract.Requires(Count >= 0)
            Contract.Requires(Count < CType(Me, IArray).Count)
            Return 0 '
        End Get
    End Property

    Sub Clear() Implements IArray.Clear
        Contract.Ensures(CType(Me, IArray).Count = 0)

    End Sub 'IArray.Clear


    Sub Insert(ByVal index As Integer, ByVal value As [Object]) Implements IArray.Insert
        Contract.Requires(index >= 0)
        Contract.Requires(index <= CType(Me, IArray).Count) ' For inserting immediately after the end.
        Contract.Ensures(CType(Me, IArray).Count = Contract.OldValue(CType(Me, IArray).Count) + 1)

    End Sub 'IArray.Insert


    Sub RemoveAt(ByVal index As Integer) Implements IArray.RemoveAt
        Contract.Requires(index >= 0)
        Contract.Requires(index < CType(Me, IArray).Count)
        Contract.Ensures(CType(Me, IArray).Count = Contract.OldValue(CType(Me, IArray).Count) - 1)

    End Sub 'IArray.RemoveAt
End Class 'IArrayContract

using System;
using System.Diagnostics.Contracts;

// An IArray is an ordered collection of objects.    
[ContractClass(typeof(IArrayContract))]
public interface IArray
{
    // The Item property provides methods to read and edit entries in the array.
    Object this[int index]
    {
        get;
        set;
    }

    int Count
    {
        get;

    }

    // Adds an item to the list.  
    // The return value is the position the new element was inserted in.
    int Add(Object value);

    // Removes all items from the list.
    void Clear();

    // Inserts value into the array at position index.
    // index must be non-negative and less than or equal to the 
    // number of elements in the array.  If index equals the number
    // of items in the array, then value is appended to the end.
    void Insert(int index, Object value);


    // Removes the item at position index.
    void RemoveAt(int index);
}

[ContractClassFor(typeof(IArray))]
internal abstract class IArrayContract : IArray
{
    int IArray.Add(Object value)
    {
        // Returns the index in which an item was inserted.
        Contract.Ensures(Contract.Result<int>() >= -1);
        Contract.Ensures(Contract.Result<int>() < ((IArray)this).Count);
        return default(int);
    }
    Object IArray.this[int index]
    {
        get
        {
            Contract.Requires(index >= 0);
            Contract.Requires(index < ((IArray)this).Count);
            return default(int);
        }
        set
        {
            Contract.Requires(index >= 0);
            Contract.Requires(index < ((IArray)this).Count);
        }
    }
    public int Count
    {
        get
        {
            Contract.Requires(Count >= 0);
            Contract.Requires(Count < ((IArray)this).Count);
            return default(int);
        }
    }

    void IArray.Clear()
    {
        Contract.Ensures(((IArray)this).Count == 0);
    }

    void IArray.Insert(int index, Object value)
    {
        Contract.Requires(index >= 0);
        Contract.Requires(index <= ((IArray)this).Count);  // For inserting immediately after the end.
        Contract.Ensures(((IArray)this).Count == Contract.OldValue(((IArray)this).Count) + 1);
    }

    void IArray.RemoveAt(int index)
    {
        Contract.Requires(index >= 0);
        Contract.Requires(index < ((IArray)this).Count);
        Contract.Ensures(((IArray)this).Count == Contract.OldValue(((IArray)this).Count) - 1);
    }
}