コード コントラクトCode Contracts

コード コントラクトを使用すると、事前条件、事後条件、およびオブジェクト不変条件をコードで指定できます。Code contracts provide a way to specify preconditions, postconditions, and object invariants in your code. 事前条件とは、メソッドやプロパティに入るときに満たされている必要がある要件です。Preconditions are requirements that must be met when entering a method or property. 事後条件は、メソッドやプロパティのコードが終了するときの予測を表します。Postconditions describe expectations at the time the method or property code exits. オブジェクト不変条件は、正しい状態のクラスに対して予期される状態を表します。Object invariants describe the expected state for a class that is in a good state.

コード コントラクトには、コードをマーク付けするためのクラス、コンパイル時の分析のための静的アナライザー、およびランタイム アナライザーが含まれます。Code contracts include classes for marking your code, a static analyzer for compile-time analysis, and a runtime analyzer. コード コントラクトのクラスは System.Diagnostics.Contracts 名前空間にあります。The classes for code contracts can be found in the System.Diagnostics.Contracts namespace.

コード コントラクトには次のような利点があります。The benefits of code contracts include the following:

  • テストの強化。コード コントラクトは、コントラクトの静的検証、ランタイム チェック、およびドキュメントの生成を提供します。Improved testing: Code contracts provide static contract verification, runtime checking, and documentation generation.

  • 自動テスト ツール:コード コントラクトを使用して、前提条件を満たさない無意味なテスト引数をフィルター処理して意味のある単体テストを生成することができます。Automatic testing tools: You can use code contracts to generate more meaningful unit tests by filtering out meaningless test arguments that do not satisfy preconditions.

  • 静的検証:静的チェックでは、プログラムを実行せず、コントラクト違反があるかどうかを決定できます。Static verification: The static checker can decide whether there are any contract violations without running the program. 暗黙的なコントラクト (null の逆参照、配列の範囲など) と明示的なコントラクトがチェックされます。It checks for implicit contracts, such as null dereferences and array bounds, and explicit contracts.

  • リファレンス ドキュメント。ドキュメントの生成は、既存の XML ドキュメント ファイルにコントラクトの情報を補強します。Reference documentation: The documentation generator augments existing XML documentation files with contract information. 生成されるドキュメントのページにコントラクトのセクションが含まれるようにするための、Sandcastle で使用できるスタイル シートも用意されています。There are also style sheets that can be used with Sandcastle so that the generated documentation pages have contract sections.

コントラクトは、すべての .NET Framework 言語ですぐに使用できます。特別なパーサーやコンパイラを記述する必要はありません。All .NET Framework languages can immediately take advantage of contracts; you do not have to write a special parser or compiler. 実行するコード コントラクト分析のレベルを指定できる Visual Studio アドインや、A Visual Studio add-in lets you specify the level of code contract analysis to be performed. コントラクトの形式が正しいかどうかを確認したり (型チェックおよび名前解決)、コンパイルされた形式 (MSIL (Microsoft Intermediate Language) 形式) のコントラクトを生成したりできるアナライザーも用意されています。The analyzers can confirm that the contracts are well-formed (type checking and name resolution) and can produce a compiled form of the contracts in Microsoft intermediate language (MSIL) format. Visual Studio でコントラクトを作成する場合は、Visual Studio の標準の IntelliSense も利用できます。Authoring contracts in Visual Studio lets you take advantage of the standard IntelliSense provided by the tool.

コントラクト クラスのほとんどのメソッドは、条件付きでコンパイルされます。したがって、それらのメソッドの呼び出しは、#define ディレクティブを使用して CONTRACTS_FULL という特別なシンボルを定義した場合にのみコンパイラで生成されます。Most methods in the contract class are conditionally compiled; that is, the compiler emits calls to these methods only when you define a special symbol, CONTRACTS_FULL, by using the #define directive. CONTRACTS_FULL を使用すると、コードで #ifdef ディレクティブを使用せずにコントラクトを記述して、コントラクトを含むものと含まないものなど、さまざまなビルドを生成できます。CONTRACTS_FULL lets you write contracts in your code without using #ifdef directives; you can produce different builds, some with contracts, and some without.

コード コントラクトを使用するためのツールおよび詳細な手順については、MSDN DevLabs Web サイトの「Code Contracts」(コード コントラクト) を参照してください。For tools and detailed instructions for using code contracts, see Code Contracts on the MSDN DevLabs Web site.

前提条件Preconditions

事前条件を指定するには、Contract.Requires メソッドを使用します。You can express preconditions by using the Contract.Requires method. 事前条件では、メソッドが呼び出される状態を指定します。Preconditions specify state when a method is invoked. 通常は、有効なパラメーター値を指定するために使用されます。They are generally used to specify valid parameter values. 事前条件で参照されるすべてのメンバーは、アクセス レベルが少なくともメソッド自体と同じである必要があります。そうでない場合、メソッドのすべての呼び出し元がその事前条件を理解できない場合があります。All members that are mentioned in preconditions must be at least as accessible as the method itself; otherwise, the precondition might not be understood by all callers of a method. また、条件に副作用がないようにする必要もあります。The condition must have no side-effects. 事前条件が満たされなかった場合の実行時の動作は、ランタイム アナライザーによって決定されます。The run-time behavior of failed preconditions is determined by the runtime analyzer.

たとえば、次の事前条件は、パラメーター x が null 以外である必要があることを表しています。For example, the following precondition expresses that parameter x must be non-null.

Contract.Requires(x != null);

事前条件が満たされなかった場合に特定の例外をスローする必要がある場合には、次のように、Requires のジェネリック オーバーロードを使用します。If your code must throw a particular exception on failure of a precondition, you can use the generic overload of Requires as follows.

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

レガシ requires ステートメントLegacy Requires Statements

ほとんどのコードには、if-then-throw コードの形式のパラメーター検証が含まれています。Most code contains some parameter validation in the form of if-then-throw code. 以下の場合は、それらのステートメントがコントラクト ツールで事前条件として認識されます。The contract tools recognize these statements as preconditions in the following cases:

  • それらのステートメントがメソッド内で他のステートメントより前にある場合。The statements appear before any other statements in a method.

  • それらのステートメント全体の後に Contract メソッドの明示的な呼び出し (RequiresEnsuresEnsuresOnThrow、または EndContractBlock のいずれかのメソッドの呼び出しなど) がある場合。The entire set of such statements is followed by an explicit Contract method call, such as a call to the Requires, Ensures, EnsuresOnThrow, or EndContractBlock method.

if-then-throw ステートメントがこのような形式になっている場合、それらのステートメントはレガシ requires ステートメントとして認識されます。When if-then-throw statements appear in this form, the tools recognize them as legacy requires statements. if-then-throw というシーケンスの後に他のコントラクトがない場合は、Contract.EndContractBlock メソッドでコードを終了します。If no other contracts follow the if-then-throw sequence, end the code with the Contract.EndContractBlock method.

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

上のテストの条件は否定の事前条件であることに注意してください。Note that the condition in the preceding test is a negated precondition. (実際の事前条件は x != null です)。否定の事前は、高度に制限されます。前の例で示すように記述する必要があります。いいえを含める必要があります、else句、およびの本文、then句は、1 つである必要がありますthrowステートメント。(The actual precondition would be x != null.) A negated precondition is highly restricted: It must be written as shown in the previous example; that is, it should contain no else clauses, and the body of the then clause must be a single throw statement. if テストには純粋性と可視性の両方の規則が適用されますが (「使用方法のガイドライン」を参照)、throw 式に適用されるのは純粋性の規則だけです。The if test is subject to both purity and visibility rules (see Usage Guidelines), but the throw expression is subject only to purity rules. ただし、スローされる例外の型には、そのコントラクトが存在するメソッドと同じレベルの可視性が必要です。However, the type of the exception thrown must be as visible as the method in which the contract occurs.

実行後の状態Postconditions

事後条件は、メソッドの終了時の状態についてのコントラクトで、Postconditions are contracts for the state of a method when it terminates. メソッドが終了する直前にチェックされます。The postcondition is checked just before exiting a method. 事後条件が満たされなかった場合の実行時の動作は、ランタイム アナライザーによって決定されます。The run-time behavior of failed postconditions is determined by the runtime analyzer.

事後条件では、事前条件とは違って、可視性のレベルがメソッドより低いメンバーも参照できます。Unlike preconditions, postconditions may reference members with less visibility. 事後条件でプライベートの状態を使用して指定した情報は、クライアントが理解できなかったり利用できなかったりする場合もありますが、そのためにクライアントがメソッドを正しく使用できなくなることはありません。A client may not be able to understand or make use of some of the information expressed by a postcondition using private state, but this does not affect the client's ability to use the method correctly.

標準の事後条件Standard Postconditions

標準の事後条件を指定するには、Ensures メソッドを使用します。You can express standard postconditions by using the Ensures method. 事後条件は、メソッドが正常に終了した場合に true になる必要がある条件を表します。Postconditions express a condition that must be true upon normal termination of the method.

Contract.Ensures(this.F > 0);

例外の事後条件Exceptional Postconditions

例外の事後条件とは、メソッドによって特定の例外がスローされた場合に true になる必要がある事後条件です。Exceptional postconditions are postconditions that should be true when a particular exception is thrown by a method. これらの事後条件を指定するには、次の例で示されているように、Contract.EnsuresOnThrow メソッドを使用します。You can specify these postconditions by using the Contract.EnsuresOnThrow method, as the following example shows.

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

引数は、T のサブタイプである例外がスローされた場合に true になる必要がある条件です。The argument is the condition that must be true whenever an exception that is a subtype of T is thrown.

例外型の中には、例外の事後条件で使用するのが困難なものもあります。There are some exception types that are difficult to use in an exceptional postcondition. たとえば、T に対して Exception 型を使用する場合は、指定する条件が、スローされる例外の型に関係なく (スタック オーバーフローなどの制御不可能な例外の場合でも) メソッドによって保証される必要があります。For example, using the type Exception for T requires the method to guarantee the condition regardless of the type of exception that is thrown, even if it is a stack overflow or other impossible-to-control exception. 例外の事後条件は、メンバーが呼び出されたときにスローされる可能性がある特定の例外に対してのみ使用するようにしてください (TimeZoneInfo メソッドの呼び出しに対して InvalidTimeZoneException がスローされる場合など)。You should use exceptional postconditions only for specific exceptions that might be thrown when a member is called, for example, when an InvalidTimeZoneException is thrown for a TimeZoneInfo method call.

特殊な事後条件Special Postconditions

次のメソッドは、事後条件の中でのみ使用できます。The following methods may be used only within postconditions:

  • 事後条件でメソッドの戻り値を参照するには、Contract.Result<T>() という式を使用します。T はメソッドの戻り値の型に置き換えられます。You can refer to method return values in postconditions by using the expression Contract.Result<T>(), where T is replaced by the return type of the method. コンパイラが型を推論できない場合は明示的に指定する必要があります。When the compiler is unable to infer the type, you must explicitly provide it. たとえば、C#コンパイラができないため、次の事後条件が必要があります、引数を受け取らないメソッドの型を推論します。Contract.Ensures(0 <Contract.Result<int>()) 戻り値の型を持つメソッドvoidは参照できませんContract.Result<T>()事後条件でします。For example, the C# compiler is unable to infer types for methods that do not take any arguments, so it requires the following postcondition: Contract.Ensures(0 <Contract.Result<int>()) Methods with a return type of void cannot refer to Contract.Result<T>() in their postconditions.

  • 事後条件の前の状態の値は、メソッドまたはプロパティの開始時の式の値を表します。A prestate value in a postcondition refers to the value of an expression at the start of a method or property. 使用される式は Contract.OldValue<T>(e) で、Te の型です。It uses the expression Contract.OldValue<T>(e), where T is the type of e. その型をコンパイラが推論できる場合は、このジェネリック型引数を省略できますYou can omit the generic type argument whenever the compiler is able to infer its type. (たとえば、この式は引数を受け取るため、C# コンパイラでは常に型が推論されます)。e に使用できる値と、古い式を使用できるコンテキストについては、いくつかの制限があります。(For example, the C# compiler always infers the type because it takes an argument.) There are several restrictions on what can occur in e and the contexts in which an old expression may appear. まず、古い式に別の古い式を含めることはできません。An old expression cannot contain another old expression. また、最も重要な点として、古い式で参照する値は、メソッドの事前条件の状態に存在する必要があります。Most importantly, an old expression must refer to a value that existed in the method's precondition state. つまり、古い式は、メソッドの事前条件が true であれば評価できる式である必要があります。In other words, it must be an expression that can be evaluated as long as the method's precondition is true. この規則のいくつかの例を次に示します。Here are several instances of that rule.

    • 値がメソッドの事前条件の状態に存在する必要があります。The value must exist in the method's precondition state. オブジェクトのフィールドを参照するには前提条件は、オブジェクトが null 以外では常に保証する必要があります。In order to reference a field on an object, the preconditions must guarantee that the object is always non-null.

    • 古い式でメソッドの戻り値を参照することはできません。You cannot refer to the method's return value in an old expression:

      Contract.OldValue(Contract.Result<int>() + x) // ERROR
      
    • 古い式で out パラメーターを参照することはできません。You cannot refer to out parameters in an old expression.

    • 量指定子の範囲がメソッドの戻り値に依存する場合は、量指定子のバインド変数に依存する古い式は使用できません。An old expression cannot depend on the bound variable of a quantifier if the range of the quantifier depends on the return value of the method:

      Contract.ForAll(0, Contract.Result<int>(), i => Contract.OldValue(xs[i]) > 3); // ERROR
      
    • 古い式で ForAll または Exists の呼び出しの匿名デリゲートのパラメーターを参照することはできません (メソッド呼び出しのインデクサーまたは引数として使用されている場合を除く)。An old expression cannot refer to the parameter of the anonymous delegate in a ForAll or Exists call unless it is used as an indexer or argument to a method call:

      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 メソッドの引数である場合を除く)。An old expression cannot occur in the body of an anonymous delegate if the value of the old expression depends on any of the parameters of the anonymous delegate, unless the anonymous delegate is an argument to the ForAll or Exists method:

      Method(... (T t) => Contract.OldValue(... t ...) ...); // ERROR
      
    • コントラクトはメソッド本体の前にあるため、Out パラメーターは問題になります。ほとんどのコンパイラでは、事後条件で out パラメーターを参照することは許可されていません。Out parameters present a problem because contracts appear before the body of the method, and most compilers do not allow references to out parameters in postconditions. この問題を解決するために、Contract クラスには ValueAtReturn メソッドが用意されています。このメソッドを使用すると、out パラメーターに基づく事後条件を使用できます。To solve this problem, the Contract class provides the ValueAtReturn method, which allows a postcondition based on an out parameter.

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

      OldValue メソッドと同様に、コンパイラが型を推論できる場合はジェネリック型パラメーターを省略できます。As with the OldValue method, you can omit the generic type parameter whenever the compiler is able to infer its type. このメソッドの呼び出しは、コントラクト リライターによって out パラメーターの値に置き換えられます。The contract rewriter replaces the method call with the value of the out parameter. ValueAtReturn メソッドは事後条件でしか使用できません。The ValueAtReturn method may appear only in postconditions. このメソッドの引数は、out パラメーターか、構造体の out パラメーターのフィールドThe argument to the method must be an out parameter or a field of a structure out parameter. (構造体コンストラクターの事後条件でフィールドを参照する場合にも便利です) でなければなりません。The latter is also useful when referring to fields in the postcondition of a structure constructor.

      注意

      現在、コード コントラクト分析ツールでは、out パラメーターが正しく初期化されているかどうかはチェックされません。事後条件に含まれていても無視されます。Currently, the code contract analysis tools do not check whether out parameters are initialized properly and disregard their mention in the postcondition. したがって、前の例で、コントラクトの後の行で x に整数を代入せずにこの値をそのまま使用しても、コンパイラで適切なエラーが生成されません。Therefore, in the previous example, if the line after the contract had used the value of x instead of assigning an integer to it, a compiler would not issue the correct error. ただし、CONTRACTS_FULL プリプロセッサ シンボルが定義されていないビルド (リリース ビルドなど) では、コンパイラでエラーが生成されます。However, on a build where the CONTRACTS_FULL preprocessor symbol is not defined (such asa release build), the compiler will issue an error.

インバリアントInvariants

オブジェクト不変条件とは、そのオブジェクトがクライアントに表示される場合に常にクラスの各インスタンスに対して true になる必要があり、Object invariants are conditions that should be true for each instance of a class whenever that object is visible to a client. オブジェクトが正しいと見なされる条件を表します。They express the conditions under which the object is considered to be correct.

インバリアントなメソッドは、ContractInvariantMethodAttribute 属性でマークされることによって識別されます。The invariant methods are identified by being marked with the ContractInvariantMethodAttribute attribute. インバリアントなメソッドには、Invariant メソッドの一連の呼び出し以外のコードが含まれていない必要があります。それらの呼び出しでは、次の例のように、個々の不変式を指定します。The invariant methods must contain no code except for a sequence of calls to the Invariant method, each of which specifies an individual invariant, as shown in the following example.

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

不変式は、CONTRACTS_FULL プリプロセッサ シンボルによって条件付きで定義され、Invariants are conditionally defined by the CONTRACTS_FULL preprocessor symbol. ランタイム チェックで各パブリック メソッドの最後にチェックされます。During run-time checking, invariants are checked at the end of each public method. 不変式が同じクラスのパブリック メソッドを参照している場合は、通常ならそのパブリック メソッドの最後に実行される不変式のチェックが無効になり、If an invariant mentions a public method in the same class, the invariant check that would normally happen at the end of that public method is disabled. そのクラスの一番外側のメソッド呼び出しの最後にのみチェックが実行されます。Instead, the check occurs only at the end of the outermost method call to that class. 別のクラスのメソッドの呼び出しのためにクラスへの再入がなされる場合も同様です。This also happens if the class is re-entered because of a call to a method on another class. オブジェクトをファイナライザーの不変性はチェックされず、IDisposable.Dispose実装します。Invariants are not checked for an object finalizer and an IDisposable.Dispose implementation.

使用方法のガイドラインUsage Guidelines

コントラクトの順序Contract Ordering

メソッドのコントラクトを記述する際に使用する必要がある要素の順序を次の表に示します。The following table shows the order of elements you should use when you write method contracts.

If-then-throw statements 下位互換性のあるパブリックな事前条件。Backward-compatible public preconditions
Requires すべてのパブリックな事前条件。All public preconditions.
Ensures すべてのパブリックな (標準の) 事後条件。All public (normal) postconditions.
EnsuresOnThrow すべてのパブリックな例外の事後条件。All public exceptional postconditions.
Ensures すべてのプライベートな/内部の (標準の) 事後条件。All private/internal (normal) postconditions.
EnsuresOnThrow すべてのプライベートな/内部の例外の事後条件。All private/internal exceptional postconditions.
EndContractBlock if-then-throw スタイルの事前条件を他のコントラクトなしで使用する場合は、EndContractBlock を呼び出して、前の if チェックがすべて事前条件であることを示します。If using if-then-throw style preconditions without any other contracts, place a call to EndContractBlock to indicate that all previous if checks are preconditions.

純粋性Purity

コントラクトの中で呼び出されるメソッドは、すべて純粋である (既存の状態を更新しない) 必要があります。All methods that are called within a contract must be pure; that is, they must not update any preexisting state. メソッドに入った後に作成されたオブジェクトは、そのピュア メソッドによって変更できます。A pure method is allowed to modify objects that have been created after entry into the pure method.

コード コントラクト ツールでは、現在、次のコード要素が純粋と見なされます。Code contract tools currently assume that the following code elements are pure:

  • PureAttribute でマークされたメソッド。Methods that are marked with the PureAttribute.

  • PureAttribute でマークされた型 (この属性はその型のすべてのメソッドに適用されます)。Types that are marked with the PureAttribute (the attribute applies to all the type's methods).

  • プロパティの get アクセサー。Property get accessors.

  • 演算子 (名前が "op" で始まり、1 つか 2 つのパラメーターを持ち、戻り値の型が void ではない静的メソッド)。Operators (static methods whose names start with "op", and that have one or two parameters and a non-void return type).

  • 完全修飾名が "System.Diagnostics.Contracts.Contract"、"System.String"、"System.IO.Path"、または "System.Type" で始まるメソッド。Any method whose fully qualified name begins with "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path", or "System.Type".

  • 呼び出されたデリゲート (デリゲート型自体に PureAttribute 属性が設定されている場合)。Any invoked delegate, provided that the delegate type itself is attributed with the PureAttribute. デリゲート型の System.Predicate<T>System.Comparison<T> は純粋と見なされます。The delegate types System.Predicate<T> and System.Comparison<T> are considered pure.

可視性Visibility

コントラクトで参照されるすべてのメンバーには、少なくとも親のメソッドと同じレベルの可視性が必要です。All members mentioned in a contract must be at least as visible as the method in which they appear. たとえば、パブリック メソッドの事前条件でプライベート フィールドを参照することはできません。そのようなコントラクトは、クライアントがメソッドの呼び出しの前に検証できません。For example, a private field cannot be mentioned in a precondition for a public method; clients cannot validate such a contract before they call the method. ただし、そのフィールドが ContractPublicPropertyNameAttribute でマークされている場合は、これらの規則から除外されます。However, if the field is marked with the ContractPublicPropertyNameAttribute, it is exempt from these rules.

Example

次に、コード コントラクトの使用例を示します。The following example shows the use of code contracts.

#define CONTRACTS_FULL

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);
    }
}
#Const CONTRACTS_FULL = True

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