ContractClassForAttribute Class

Definition

Namespace:

System.Diagnostics.Contracts

Assembly:

System.Diagnostics.Contracts.dll

Source:

Contracts.cs

Specifies that a class is a contract for a type.

public ref class ContractClassForAttribute sealed : Attribute

[System.AttributeUsage(System.AttributeTargets.Class, AllowMultiple=false, Inherited=false)]
[System.Diagnostics.Conditional("CONTRACTS_FULL")]
public sealed class ContractClassForAttribute : Attribute

[<System.AttributeUsage(System.AttributeTargets.Class, AllowMultiple=false, Inherited=false)>]
[<System.Diagnostics.Conditional("CONTRACTS_FULL")>]
type ContractClassForAttribute = class
    inherit Attribute

Public NotInheritable Class ContractClassForAttribute
Inherits Attribute

Inheritance

Object

Attribute

ContractClassForAttribute

Attributes

AttributeUsageAttribute ConditionalAttribute

Examples

The following example shows how to use the ContractClassForAttribute attribute to specify the contracts for another type. This code example is part of a larger example provided for the ContractClassAttribute class.

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

Remarks

Types that are marked with this attribute represent a code contract for another type. The type that the contract applies to is specified in the constructor.

Constructors

ContractClassForAttribute(Type)

Initializes a new instance of the ContractClassForAttribute class, specifying the type the current class is a contract for.

Properties

TypeContractsAreFor	Gets the type that this code contract applies to.
TypeId	When implemented in a derived class, gets a unique identifier for this Attribute. (Inherited from Attribute)

Methods

Equals(Object)	Returns a value that indicates whether this instance is equal to a specified object. (Inherited from Attribute)
GetHashCode()	Returns the hash code for this instance. (Inherited from Attribute)
GetType()	Gets the Type of the current instance. (Inherited from Object)
IsDefaultAttribute()	When overridden in a derived class, indicates whether the value of this instance is the default value for the derived class. (Inherited from Attribute)
Match(Object)	When overridden in a derived class, returns a value that indicates whether this instance equals a specified object. (Inherited from Attribute)
MemberwiseClone()	Creates a shallow copy of the current Object. (Inherited from Object)
ToString()	Returns a string that represents the current object. (Inherited from Object)

See also

• ContractClassAttribute