Contrats de codeCode Contracts

Les contrats de code offrent un moyen de spécifier des conditions préalables, des post-conditions et des invariants d'objet dans votre code.Code contracts provide a way to specify preconditions, postconditions, and object invariants in your code. Les conditions préalables sont des exigences qui doivent être satisfaites à l'entrée d'une méthode ou d'une propriété.Preconditions are requirements that must be met when entering a method or property. Les post-conditions décrivent les attentes à la sortie de la méthode ou de la propriété.Postconditions describe expectations at the time the method or property code exits. Les invariants d'objet décrivent l'état attendu pour une classe présentant un état correct.Object invariants describe the expected state for a class that is in a good state.

Les contrats de code incluent des classes pour le marquage de votre code, un analyseur statique pour l'analyse au moment de la compilation, ainsi qu'un analyseur au moment de l'exécution.Code contracts include classes for marking your code, a static analyzer for compile-time analysis, and a runtime analyzer. Les classes des contrats de code se trouvent dans l'espace de noms System.Diagnostics.Contracts.The classes for code contracts can be found in the System.Diagnostics.Contracts namespace.

Les contrats de code offrent les avantages suivants :The benefits of code contracts include the following:

  • Tests améliorés : les contrats de code permettent la vérification de contrat statique, la vérification au moment de l'exécution et la génération de documentation.Improved testing: Code contracts provide static contract verification, runtime checking, and documentation generation.

  • Outils de test automatique : vous pouvez utiliser les contrats de code pour générer des tests unitaires plus explicites en filtrant les arguments de test sans signification qui ne remplissent pas les conditions préalables.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.

  • Vérification statique : le vérificateur statique peut déterminer s'il existe des violations de contrat sans exécuter le programme.Static verification: The static checker can decide whether there are any contract violations without running the program. Il recherche des contrats implicites, tels que des déréférencements et des limites de tableau null, ainsi que des contrats explicites.It checks for implicit contracts, such as null dereferences and array bounds, and explicit contracts.

  • Documentation de référence : le générateur de documentation complète les fichiers de documentation XML existants avec des informations de contrat.Reference documentation: The documentation generator augments existing XML documentation files with contract information. Des feuilles de style peuvent également être utilisées avec Sandcastle pour ajouter des sections de contrat dans les pages de documentation générées.There are also style sheets that can be used with Sandcastle so that the generated documentation pages have contract sections.

Tous les langages .NET Framework peuvent directement utiliser les contrats, sans que vous ayez besoin de développer un analyseur ou compilateur spécial.All .NET Framework languages can immediately take advantage of contracts; you do not have to write a special parser or compiler. Un complément Visual Studio vous permet de spécifier le niveau d'analyse de contrats de code à effectuer.A Visual Studio add-in lets you specify the level of code contract analysis to be performed. Les analyseurs peuvent vérifier que les contrats sont correctement écrits (contrôle de type et résolution de noms), et créer un formulaire compilé des contrats au format 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. La création de contrats dans Visual Studio vous permet de tirer parti de la fonctionnalité IntelliSense standard fournie par l'outil.Authoring contracts in Visual Studio lets you take advantage of the standard IntelliSense provided by the tool.

La plupart des méthodes dans la classe de contrat sont compilées de façon conditionnelle, à savoir que le compilateur effectue des appels à ces méthodes uniquement si vous définissez le symbole spécial CONTRACTS_FULL à l'aide de la directive #define.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. Avec CONTRACTS_FULL, vous pouvez écrire des contrats dans votre code sans utiliser de directives #ifdef, et générer ainsi différentes builds, avec et sans contrats.CONTRACTS_FULL lets you write contracts in your code without using #ifdef directives; you can produce different builds, some with contracts, and some without.

Pour télécharger les outils et obtenir des instructions détaillées sur l’utilisation des contrats de code, consultez Contrats de code sur le site web MSDN DevLabs.For tools and detailed instructions for using code contracts, see Code Contracts on the MSDN DevLabs Web site.

PreconditionsPreconditions

Vous pouvez spécifier des conditions préalables à l'aide de la méthode Contract.Requires.You can express preconditions by using the Contract.Requires method. Les conditions préalables définissent l'état à l'appel d'une méthode.Preconditions specify state when a method is invoked. Elles sont généralement utilisées pour indiquer des valeurs de paramètre valides.They are generally used to specify valid parameter values. Tous les membres spécifiés dans les conditions préalables doivent être au moins aussi accessibles que la méthode elle-même. Autrement, la condition préalable risque de ne pas être comprise par tous les appelants de la méthode.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. La condition ne doit pas avoir d'effets secondaires.The condition must have no side-effects. Le comportement au moment de l'exécution des conditions préalables non réussies est déterminé par l'analyseur au moment de l'exécution.The run-time behavior of failed preconditions is determined by the runtime analyzer.

Par exemple, la condition préalable suivante spécifie que le paramètre x ne doit pas être null.For example, the following precondition expresses that parameter x must be non-null.

Contract.Requires( x != null );

Si votre code doit lever une exception particulière en cas d'échec d'une condition préalable, utilisez la surcharge générique de Requires comme suit.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" );

Instructions Requires héritéesLegacy Requires Statements

Dans la plupart des cas, le code contient du code de validation de paramètres sous la forme d’instructions if-then-throw.Most code contains some parameter validation in the form of if-then-throw code. Les outils de contrat reconnaissent ces instructions comme étant des conditions préalables dans les cas suivants :The contract tools recognize these statements as preconditions in the following cases:

Quand les instructions if-then-throw apparaissent sous cette forme, les outils les reconnaissent en tant qu’instructions requires héritées.When if-then-throw statements appear in this form, the tools recognize them as legacy requires statements. Si aucun autre contrat ne suit la séquence if-then-throw, terminez le code par la méthode 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  

Notez que la condition du test précédent est une condition préalable négativeNote that the condition in the preceding test is a negated precondition. (la condition préalable réelle serait x != null). Une condition préalable négative est très restreinte. Elle doit être écrite comme indiqué dans l'exemple précédent, à savoir qu'elle ne doit pas contenir de clauses else, et le corps de la clause then doit se composer d'une seule instruction 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. Le test if est soumis aux règles de pureté et à celles de visibilité (voir Indications relatives à l’utilisation), mais l’expression throw est soumise uniquement aux règles de pureté.The if test is subject to both purity and visibility rules (see Usage Guidelines), but the throw expression is subject only to purity rules. Toutefois, le type de l'exception levée doit être aussi visible que la méthode dans laquelle le contrat se produit.However, the type of the exception thrown must be as visible as the method in which the contract occurs.

Post-conditionsPostconditions

Les post-conditions sont des contrats relatifs à l'état d'une méthode qui se termine.Postconditions are contracts for the state of a method when it terminates. La post-condition est vérifiée juste avant la sortie de la méthode.The postcondition is checked just before exiting a method. Le comportement au moment de l'exécution des post-conditions non réussies est déterminé par l'analyseur au moment de l'exécution.The run-time behavior of failed postconditions is determined by the runtime analyzer.

Contrairement aux conditions préalables, les post-conditions peuvent référencer des membres ayant moins de visibilité.Unlike preconditions, postconditions may reference members with less visibility. Il est possible qu'un client ne puisse pas comprendre ou utiliser certaines des informations spécifiées par une post-condition avec un état privé, mais cela n'empêche pas le client d'utiliser la méthode correctement.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.

Post-conditions standardStandard Postconditions

Vous pouvez spécifier les post-conditions standard à l'aide de la méthode Ensures.You can express standard postconditions by using the Ensures method. Les post-conditions expriment une condition qui doit être true à l'arrêt normal de la méthode.Postconditions express a condition that must be true upon normal termination of the method.

Contract.Ensures( this.F > 0 );

Post-conditions exceptionnellesExceptional Postconditions

Les post-conditions exceptionnelles sont des post-conditions qui doivent être true quand une exception particulière est levée par une méthode.Exceptional postconditions are postconditions that should be true when a particular exception is thrown by a method. Vous pouvez les spécifier à l'aide de la méthode Contract.EnsuresOnThrow, comme le montre l'exemple suivant.You can specify these postconditions by using the Contract.EnsuresOnThrow method, as the following example shows.

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

L'argument est la condition qui doit être true chaque fois qu'une exception qui est un sous-type de T est levée.The argument is the condition that must be true whenever an exception that is a subtype of T is thrown.

Certains types d'exception sont difficiles à utiliser dans une post-condition exceptionnelle.There are some exception types that are difficult to use in an exceptional postcondition. Par exemple, l'utilisation du type Exception pour T nécessite que la méthode garantisse la condition indépendamment du type d'exception levée, même s'il s'agit d'un dépassement de capacité de la pile ou d'une autre exception impossible à contrôler.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. Utilisez les post-conditions exceptionnelles uniquement pour des exceptions spécifiques qui peuvent être levées après l'appel d'un membre, par exemple, quand une exception InvalidTimeZoneException est levée pour un appel de méthode TimeZoneInfo.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.

Post-conditions spécialesSpecial Postconditions

Les méthodes suivantes peuvent être utilisées uniquement au sein de post-conditions :The following methods may be used only within postconditions:

  • Vous pouvez faire référence aux valeurs de retour de la méthode dans les post-conditions à l'aide de l'expression Contract.Result<T>(), où T est remplacé par le type de retour de la méthode.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. Si le compilateur ne peut pas déduire le type, vous devez le fournir explicitement.When the compiler is unable to infer the type, you must explicitly provide it. Par exemple, le compilateur C# ne peut pas déduire les types des méthodes qui ne prennent pas d'arguments. Il nécessite donc la post-condition suivante : Contract.Ensures(0 <Contract.Result<int>()). Les méthodes possédant le type de retour void ne peuvent pas faire référence à Contract.Result<T>() dans leurs post-conditions.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.

  • Une valeur de « pré-état » dans une post-condition fait référence à la valeur d'une expression au début d'une méthode ou d'une propriété.A prestate value in a postcondition refers to the value of an expression at the start of a method or property. Elle utilise l'expression Contract.OldValue<T>(e), où T est le type de e.It uses the expression Contract.OldValue<T>(e), where T is the type of e. Vous pouvez omettre l'argument de type générique chaque fois que le compilateur est en mesure de déduire son typeYou can omit the generic type argument whenever the compiler is able to infer its type. (par exemple, le compilateur C# déduit toujours le type quand un argument est utilisé). Il existe plusieurs restrictions sur ce qui peut se produire dans e et les contextes dans lesquels une expression ancienne peut s'afficher.(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. Une expression ancienne ne peut pas contenir une autre expression ancienne.An old expression cannot contain another old expression. Encore plus important, une expression ancienne doit faire référence à une valeur qui a existé dans l'état de condition préalable de la méthode.Most importantly, an old expression must refer to a value that existed in the method's precondition state. En d'autres termes, il doit s'agir d'une expression qui peut être évaluée tant que la condition préalable de la méthode est true.In other words, it must be an expression that can be evaluated as long as the method's precondition is true. Voici plusieurs instances de cette règle :Here are several instances of that rule.

    • La valeur doit exister dans l'état de condition préalable de la méthode.The value must exist in the method's precondition state. Pour référencer un champ sur un objet, les conditions préalables doivent garantir que cet objet a toujours une valeur non null.In order to reference a field on an object, the preconditions must guarantee that that object is always non-null.

    • Vous ne pouvez pas faire référence à la valeur de retour de la méthode dans une expression ancienne :You cannot refer to the method's return value in an old expression:

      Contract.OldValue(Contract.Result<int>() + x) // ERROR  
      
    • Vous ne pouvez pas faire référence aux paramètres out dans une expression ancienne.You cannot refer to out parameters in an old expression.

    • Une expression ancienne ne peut pas dépendre de la variable liée d'un quantificateur si la plage du quantificateur dépend de la valeur de retour de la méthode :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  
      
    • Une expression ancienne ne peut pas faire référence au paramètre du délégué anonyme dans un appel ForAll ou Exists, sauf si elle est utilisée en tant qu'indexeur ou argument pour un appel de méthode :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  
      
    • Une expression ancienne ne peut pas s'utiliser dans le corps d'un délégué anonyme si la valeur de l'expression ancienne dépend de l'un des paramètres du délégué anonyme, à moins que le délégué anonyme ne soit un argument de la méthode ForAll ou 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  
      
    • Les paramètres Out posent un problème, car les contrats sont placés avant le corps de la méthode, et la plupart des compilateurs n'autorisent pas les références aux paramètres out dans les post-conditions.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. Pour résoudre ce problème, la classe Contract fournit la méthode ValueAtReturn, qui permet d'utiliser une post-condition basée sur un paramètre 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) f  
      Contract.Ensures(Contract.ValueAtReturn(out x) == 3);  
      x = 3;  
      

      Comme avec la méthode OldValue, vous pouvez omettre le paramètre de type générique chaque fois que le compilateur est en mesure de déduire son type.As with the OldValue method, you can omit the generic type parameter whenever the compiler is able to infer its type. Le module de réécriture de contrat remplace l'appel de méthode par la valeur du paramètre out.The contract rewriter replaces the method call with the value of the out parameter. La méthode ValueAtReturn peut apparaître uniquement dans des post-conditions.The ValueAtReturn method may appear only in postconditions. L'argument de la méthode doit être un paramètre out ou un champ d'un paramètre out de structure.The argument to the method must be an out parameter or a field of a structure out parameter. Ce dernier est également utile pour faire référence aux champs dans la post-condition d'un constructeur de structure.The latter is also useful when referring to fields in the postcondition of a structure constructor.

      Note

      Actuellement, les outils d'analyse de contrat de code ne vérifient pas si les paramètres out sont correctement initialisés et ignorent leur mention dans la post-condition.Currently, the code contract analysis tools do not check whether out parameters are initialized properly and disregard their mention in the postcondition. Si, dans l'exemple précédent, la ligne après le contrat avait utilisé la valeur de x au lieu de lui assigner un nombre entier, un compilateur n'aurait donc pas généré l'erreur correspondante.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. Toutefois, dans une build où le symbole de préprocesseur CONTRACTS_FULL n’est pas défini (telle qu’une build de mise en production), le compilateur génère une erreur.However, on a build where the CONTRACTS_FULL preprocessor symbol is not defined (such asa release build), the compiler will issue an error.

InvariantsInvariants

Les invariants d'objet sont des conditions qui doivent être remplies (true) pour chaque instance d'une classe dès que cet objet est visible par un client.Object invariants are conditions that should be true for each instance of a class whenever that object is visible to a client. Ils spécifient les conditions sous lesquelles l'objet est considéré comme étant correct.They express the conditions under which the object is considered to be correct.

Les méthodes invariantes sont identifiées par l'attribut ContractInvariantMethodAttribute.The invariant methods are identified by being marked with the ContractInvariantMethodAttribute attribute. Elles ne doivent contenir aucun code à l'exception d'une séquence d'appels à la méthode Invariant, chacun spécifiant un invariant individuel, comme indiqué dans l'exemple suivant.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);  
...  
}  

Les invariants sont définis de façon conditionnelle par le symbole de préprocesseur CONTRACTS_FULL.Invariants are conditionally defined by the CONTRACTS_FULL preprocessor symbol. Ils sont vérifiés au moment de l'exécution à la fin de chaque méthode publique.During run-time checking, invariants are checked at the end of each public method. Si un invariant spécifie une méthode publique dans la même classe, la vérification d'invariant prévue normalement à la fin de cette méthode publique est désactivée.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. À la place, la vérification se produit uniquement à la fin de l'appel de méthode le plus à l'extérieur de cette classe.Instead, the check occurs only at the end of the outermost method call to that class. Cela se produit également si la classe est à nouveau entrée à cause d'un appel à une méthode sur une autre classe.This also happens if the class is re-entered because of a call to a method on another class. Les invariants ne sont pas vérifiés pour les finaliseurs d'objets ni pour les méthodes qui implémentent la méthode Dispose.Invariants are not checked for object finalizers or for any methods that implement the Dispose method.

Indications relatives à l'utilisationUsage Guidelines

Classement de contratContract Ordering

Le tableau suivant indique l'ordre des éléments à utiliser quand vous écrivez des contrats de méthode.The following table shows the order of elements you should use when you write method contracts.

If-then-throw statements Conditions préalables publiques à compatibilité descendanteBackward-compatible public preconditions
Requires Toutes les conditions préalables publiquesAll public preconditions.
Ensures Toutes les post-conditions standard publiquesAll public (normal) postconditions.
EnsuresOnThrow Toutes les post-conditions exceptionnelles publiquesAll public exceptional postconditions.
Ensures Toutes les post-conditions standard privées/internesAll private/internal (normal) postconditions.
EnsuresOnThrow Toutes les post-conditions exceptionnelles privées/internesAll private/internal exceptional postconditions.
EndContractBlock Si vous utilisez des conditions préalables de style if-then-throw sans autres contrats, ajoutez un appel à EndContractBlock pour indiquer que toutes les vérifications if précédentes sont des conditions préalables.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.

PuretéPurity

Toutes les méthodes appelées dans un contrat doivent être pures, c'est-à-dire qu'elles ne doivent pas mettre à jour un état préexistant.All methods that are called within a contract must be pure; that is, they must not update any preexisting state. Une méthode pure peut modifier des objets qui ont été créés après l'entrée dans la méthode pure.A pure method is allowed to modify objects that have been created after entry into the pure method.

Les outils de contrat de code considèrent actuellement que les éléments de code suivants sont purs :Code contract tools currently assume that the following code elements are pure:

  • Méthodes marquées avec l'attribut PureAttribute.Methods that are marked with the PureAttribute.

  • Types marqués avec l'attribut PureAttribute (cet attribut s'applique à toutes les méthodes du type).Types that are marked with the PureAttribute (the attribute applies to all the type's methods).

  • Accesseurs get de propriété.Property get accessors.

  • Opérateurs (méthodes statiques dont le nom commence par « op », qui comportent un ou deux paramètres et dont le type de retour n'est pas void).Operators (static methods whose names start with "op", and that have one or two parameters and a non-void return type).

  • Méthodes dont le nom qualifié complet commence par « System.Diagnostics.Contracts.Contract », « System.String », « System.IO.Path » ou « System.Type ».Any method whose fully qualified name begins with "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path", or "System.Type".

  • Les délégués appelés, à condition que le type délégué lui-même soit attribué avec l'attribut PureAttribute.Any invoked delegate, provided that the delegate type itself is attributed with the PureAttribute. Les types délégués System.Predicate<T> et System.Comparison<T> sont considérés comme purs.The delegate types System.Predicate<T> and System.Comparison<T> are considered pure.

VisibilitéVisibility

Tous les membres indiqués dans un contrat doivent être au moins aussi visibles que la méthode dans laquelle ils apparaissent.All members mentioned in a contract must be at least as visible as the method in which they appear. Par exemple, un champ privé ne peut pas être spécifié dans une condition préalable pour une méthode publique, car les clients ne peuvent pas valider un tel contrat avant d'appeler la méthode.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. Cependant, si le champ est marqué avec l'attribut ContractPublicPropertyNameAttribute, il est exempté de ces règles.However, if the field is marked with the ContractPublicPropertyNameAttribute, it is exempt from these rules.

ExempleExample

L'exemple suivant illustre l'utilisation des contrats de code.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