ContractClassForAttribute(Type) 생성자

정의

네임스페이스:

System.Diagnostics.Contracts

어셈블리:

System.Diagnostics.Contracts.dll

Source:

Contracts.cs

현재 클래스의 계약 형식을 지정하여 ContractClassForAttribute 클래스의 새 인스턴스를 초기화합니다.

public ContractClassForAttribute (Type typeContractsAreFor);

매개 변수

typeContractsAreFor

Type

현재 클래스의 계약 형식입니다.

설명

다음 예제에서는 형식의 계약이 인터페이스에 ContractClassAttribute 적용되도록 지정하기 위해 IArray 생성자를 사용하는 방법을 보여 줍니다. 이 코드 예제는에 대해 제공 된 큰 예제의 일부는 ContractClassAttribute 클래스입니다.

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

적용 대상