コードコントラクト

[アーティクル]
08/09/2011

コードコントラクトを使用すると、事前条件、事後条件、およびオブジェクト不変条件をコードで指定できます。事前条件とは、メソッドやプロパティに入るときに満たされている必要がある要件です。事後条件は、メソッドやプロパティのコードが終了するときの予測を表します。オブジェクト不変条件は、正しい状態のクラスに対して予期される状態を表します。

コードコントラクトには、コードをマーク付けするためのクラス、コンパイル時の分析のための静的アナライザー、およびランタイムアナライザーが含まれます。コードコントラクトのクラスは System.Diagnostics.Contracts 名前空間にあります。

コードコントラクトには次のような利点があります。

テストの強化: コードコントラクトでは、コントラクトの静的検証、ランタイムチェック、およびドキュメントの生成がサポートされます。
自動テストツール: コードコントラクトを使用すると、事前条件を満たさない無意味なテスト引数をフィルターで除外して、より意味のある単体テストを生成できます。
静的検証: 静的チェックにより、コントラクト違反がないかどうかをプログラムを実行せずに確認できます。暗黙的なコントラクト (null の逆参照、配列の範囲など) と明示的なコントラクトがチェックされます。
リファレンスドキュメント: ドキュメント生成機能により、既存の XML ドキュメントファイルにコントラクトの情報が追加されます。生成されるドキュメントのページにコントラクトのセクションが含まれるようにするための、Sandcastle で使用できるスタイルシートも用意されています。

コントラクトは、すべての .NET Framework 言語ですぐに使用できます。特別なパーサーやコンパイラを記述する必要はありません。実行するコードコントラクト分析のレベルを指定できる Visual Studio アドインや、コントラクトの形式が正しいかどうかを確認したり (型チェックおよび名前解決)、コンパイルされた形式 (MSIL (Microsoft Intermediate Language) 形式) のコントラクトを生成したりできるアナライザーも用意されています。 Visual Studio でコントラクトを作成する場合は、Visual Studio の標準の IntelliSense も利用できます。

コントラクトクラスのほとんどのメソッドは、条件付きでコンパイルされます。したがって、それらのメソッドの呼び出しは、#define ディレクティブを使用して CONTRACTS FULL という特別なシンボルを定義した場合にのみコンパイラで生成されます。 CONTRACTS FULL を使用すると、コードで #ifdef ディレクティブを使用せずにコントラクトを記述して、コントラクトを含むビルドと含まないビルドを生成できます。

コードコントラクトを使用するためのツールおよび詳細な手順については、MSDN DevLabs Web サイトの「Code Contracts (コードコントラクト)」を参照してください。

Preconditions

事前条件を指定するには、Contract.Requires メソッドを使用します。事前条件では、メソッドが呼び出される状態を指定します。通常は、有効なパラメーター値を指定するために使用されます。事前条件で参照されるすべてのメンバーは、アクセスレベルが少なくともメソッド自体と同じである必要があります。そうでないと、メソッドのすべての呼び出し元がその事前条件を理解できるない場合があります。また、条件に副作用がないようにする必要もあります。事前条件が満たされなかった場合の実行時の動作は、ランタイムアナライザーによって決定されます。

たとえば、次の事前条件は、パラメーター x が null 以外である必要があることを表しています。

Contract.Requires( x != null );

事前条件が満たされなかった場合に特定の例外をスローするには、次のように、Requires のジェネリックオーバーロードを使用します。

Contract.Requires<ArgumentNullException>( x != null, "x" );

レガシ requires ステートメント

ほとんどのコードには、if-then-throw 形式のパラメーター検証が含まれています。以下の場合は、それらのステートメントがコントラクトツールで事前条件として認識されます。

それらのステートメントがメソッド内で他のステートメントより前にある場合。
それらのステートメント全体の後に Contract メソッドの明示的な呼び出し (Requires、Ensures、EnsuresOnThrow、または EndContractBlock のいずれかのメソッドの呼び出しなど) がある場合。

if-then-throw ステートメントがこのような形式になっている場合、それらのステートメントはレガシ requires ステートメントとして認識されます。 if-then-throw というシーケンスの後に他のコントラクトがない場合は、Contract.EndContractBlock メソッドでコードを終了します。

if ( x == null ) throw new ...
Contract.EndContractBlock(); // All previous "if" checks are preconditions

上のテストの条件は否定の事前条件であることに注意してください (実際の事前条件は x != null です)。否定の事前条件には多くの制限があり、上の例のように記述する必要があります (else 句が含まれていてはいけない、then 句の本体は 1 つの throw ステートメントにするなど)。 if テストには純粋性と可視性の両方の規則が適用されますが (「使用方法のガイドライン」を参照)、throw 式に適用されるのは純粋性の規則だけです。ただし、スローされる例外の型には、そのコントラクトが存在するメソッドと同じレベルの可視性が必要です。

Postconditions

事後条件は、メソッドの終了時の状態についてのコントラクトで、メソッドが終了する直前にチェックされます。事後条件が満たされなかった場合の実行時の動作は、ランタイムアナライザーによって決定されます。

事後条件では、事前条件とは違って、可視性のレベルがメソッドより低いメンバーも参照できます。事後条件でプライベートの状態を使用して指定した情報は、クライアントが理解できなかったり利用できなかったりする場合もありますが、そのためにクライアントがメソッドを正しく使用できなくなることはありません。

標準の事後条件

標準の事後条件を指定するには、Ensures メソッドを使用します。事後条件は、メソッドが正常に終了した場合に true になる必要がある条件を表します。

Contract.Ensures( this .F > 0 );

例外の事後条件

例外の事後条件とは、メソッドによって特定の例外がスローされた場合に true になる必要がある事後条件です。これらの事後条件を指定するには、次の例のように、Contract.EnsuresOnThrow メソッドを使用します。

Contract.EnsuresOnThrow<T>( this.F > 0 );

引数は、T のサブタイプである例外がスローされた場合に true になる必要がある条件です。

例外型の中には、例外の事後条件で使用するのが困難なものもあります。たとえば、T に対して Exception 型を使用する場合は、指定する条件が、スローされる例外の型に関係なく (スタックオーバーフローなどの制御不可能な例外の場合でも) メソッドによって保証される必要があります。例外の事後条件は、メンバーが呼び出されたときにスローされる可能性がある特定の例外に対してのみ使用するようにしてください (TimeZoneInfo メソッドの呼び出しに対して InvalidTimeZoneException がスローされる場合など)。

特殊な事後条件

次のメソッドは、事後条件の中でのみ使用できます。

事後条件でメソッドの戻り値を参照するには、Contract. Result<T>() という式を使用します。T はメソッドの戻り値の型に置き換えられます。コンパイラが型を推論できない場合は明示的に指定する必要があります。たとえば、C# コンパイラでは、引数を受け取らないメソッドの型は推論できないため、Contract.Ensures(0 < Contract.Result<int>()) という事後条件を使用する必要があります。戻り値の型が void のメソッドの事後条件では Contract. Result<T>() を参照できません。

事後条件の前の状態の値は、メソッドまたはプロパティの開始時の式の値を表します。使用される式は Contract.OldValue<T>(e) で、T は e の型です。その型をコンパイラが推論できる場合は、このジェネリック型引数を省略できます (たとえば、この式は引数を受け取るため、C# コンパイラでは常に型が推論されます)。 e に使用できる値と、古い式を使用できるコンテキストについては、いくつかの制限があります。まず、古い式に別の古い式を含めることはできません。また、最も重要な点として、古い式で参照する値は、メソッドの事前条件の状態に存在する必要があります。つまり、古い式は、メソッドの事前条件が true であれば評価できる式である必要があります。この規則のいくつかの例を次に示します。

値がメソッドの事前条件の状態に存在する必要があります。オブジェクトのフィールドを参照するには、オブジェクトが常に null 以外であることが事前条件によって保証される必要があります。
古い式でメソッドの戻り値を参照することはできません。
```
Contract.OldValue(Contract.Result<int>() + x) // ERROR
```
古い式で out パラメーターを参照することはできません。
量指定子の範囲がメソッドの戻り値に依存する場合は、量指定子のバインド変数に依存する古い式は使用できません。
```
Contract. ForAll (0,Contract. Result<int>(),
i => Contract.OldValue(xs[i]) > 3 ); // ERROR
```
古い式で ForAll または Exists の呼び出しの匿名デリゲートのパラメーターを参照することはできません (メソッド呼び出しのインデクサーまたは引数として使用されている場合を除く)。
```
Contract. ForAll (0, xs .Length, i => Contract.OldValue(xs[i]) > 3); // OK
Contract. ForAll (0, xs .Length, i => Contract.OldValue(i) > 3 ); // ERROR
```
古い式の値が匿名デリゲートのパラメーターに依存している場合、古い式をその匿名デリゲートの本体に含めることはできません (匿名デリゲートが ForAll メソッドまたは Exists メソッドの引数である場合を除く)。
```
Method( ... (T t) => Contract.OldValue(... t ...) ... ); // ERROR
```

コントラクトはメソッド本体の前にあるため、Out パラメーターは問題になります。ほとんどのコンパイラでは、事後条件で out パラメーターを参照することは許可されていません。この問題を解決するために、Contract クラスには ValueAtReturn<T> メソッドが用意されています。このメソッドを使用すると、out パラメーターに基づく事後条件を使用できます。

public void OutParam(out int x) f
Contract.Ensures(Contract.ValueAtReturn(out x) == 3);
x = 3;

OldValue<T> メソッドと同様に、コンパイラが型を推論できる場合はジェネリック型パラメーターを省略できます。このメソッドの呼び出しは、コントラクトリライターによって out パラメーターの値に置き換えられます。 ValueAtReturn<T> メソッドは事後条件でしか使用できません。このメソッドの引数は、out パラメーターか、構造体の out パラメーターのフィールド (構造体コンストラクターの事後条件でフィールドを参照する場合にも便利です) である必要があります。

メモ
現在、コードコントラクト分析ツールでは、out パラメーターが正しく初期化されているかどうかはチェックされません。事後条件に含まれていても無視されます。したがって、前の例で、コントラクトの後の行で x に整数を割り当てずにこの値をそのまま使用しても、コンパイラで適切なエラーが生成されません。ただし、CONTRACTS FULL プリプロセッサシンボルが定義されていないビルド (リリースビルドなど)では、コンパイラでエラーが生成されます。

現在、コードコントラクト分析ツールでは、out パラメーターが正しく初期化されているかどうかはチェックされません。事後条件に含まれていても無視されます。したがって、前の例で、コントラクトの後の行で x に整数を割り当てずにこの値をそのまま使用しても、コンパイラで適切なエラーが生成されません。ただし、CONTRACTS FULL プリプロセッサシンボルが定義されていないビルド (リリースビルドなど)では、コンパイラでエラーが生成されます。

一定の条件

オブジェクト不変条件とは、そのオブジェクトがクライアントに表示される場合に常にクラスの各インスタンスに対して true になる必要があり、オブジェクトが正しいと見なされる条件を表します。

インバリアントなメソッドは、ContractInvariantMethodAttribute 属性でマークされることによって識別されます。インバリアントなメソッドには、Invariant メソッドの一連の呼び出し以外のコードが含まれていない必要があります。それらの呼び出しでは、次の例のように、個々の不変式を指定します。

[ContractInvariantMethod]
protected void ObjectInvariant () 
{
Contract.Invariant ( this.y >= 0 );
Contract.Invariant ( this.x > this.y );
...
}

不変式は、CONTRACTS FULL プリプロセッサシンボルによって条件付きで定義され、ランタイムチェックで各パブリックメソッドの最後にチェックされます。不変式が同じクラスのパブリックメソッドを参照している場合は、通常ならそのパブリックメソッドの最後に行われる不変式のチェックが無効になり、そのクラスの一番外側のメソッド呼び出しの最後にのみチェックが行われます。別のクラスのメソッドの呼び出しのためにクラスへの再入が行われる場合も同様です。不変式のチェックは、オブジェクトファイナライザーや、Dispose メソッドを実装するメソッドに対しては行われません。

使用方法のガイドライン

コントラクトの順序

メソッドのコントラクトを記述する際に使用する必要がある要素の順序を次の表に示します。

If-then-throw statements	下位互換性のあるパブリックな事前条件。
Requires	すべてのパブリックな事前条件。
Ensures	すべてのパブリックな (標準の) 事後条件。
EnsuresOnThrow	すべてのパブリックな例外の事後条件。
Ensures	すべてのプライベートな/内部の (標準の) 事後条件。
EnsuresOnThrow	すべてのプライベートな/内部の例外の事後条件。
EndContractBlock	if-then-throw スタイルの事前条件を他のコントラクトなしで使用する場合は、EndContractBlock を呼び出して、前の if チェックがすべて事前条件であることを示します。

純粋性

コントラクトの中で呼び出されるメソッドは、すべて純粋である (既存の状態を更新しない) 必要があります。メソッドに入った後に作成されたオブジェクトは変更できます。

コードコントラクトツールでは、現在、次のコード要素が純粋と見なされます。

PureAttribute でマークされたメソッド。
PureAttribute でマークされた型 (この属性はその型のすべてのメソッドに適用されます)。
プロパティの get アクセサー。
演算子 (名前が "op" で始まり、1 つか 2 つのパラメーターを持ち、戻り値の型が void ではない静的メソッド)。
完全修飾名が "System.Diagnostics.Contracts.Contract"、"System.String"、"System.IO.Path"、または "System.Type" で始まるメソッド。
呼び出されたデリゲート (デリゲート型自体に PureAttribute 属性が設定されている場合)。デリゲート型の System.Predicate<T> と System.Comparison<T> は純粋と見なされます。

可視性

コントラクトで参照されるすべてのメンバーには、少なくとも親のメソッドと同じレベルの可視性が必要です。たとえば、パブリックメソッドの事前条件でプライベートフィールドを参照することはできません。そのようなコントラクトは、クライアントがメソッドの呼び出しの前に検証できません。ただし、そのフィールドが ContractPublicPropertyNameAttribute でマークされている場合は、これらの規則から除外されます。

例

次に、コードコントラクトの使用例を示します。

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

Share via

コードコントラクト

Preconditions

レガシ requires ステートメント

Postconditions

標準の事後条件

例外の事後条件

特殊な事後条件

一定の条件

使用方法のガイドライン

コントラクトの順序

純粋性

可視性

例

その他のリソース

Share via

コード コントラクト

Preconditions

レガシ requires ステートメント

Postconditions

標準の事後条件

例外の事後条件

特殊な事後条件

一定の条件

使用方法のガイドライン

コントラクトの順序

純粋性

可視性

例

その他のリソース

コードコントラクト