Contratti di codiceCode Contracts

I contratti di codice consentono di specificare precondizioni, postcondizioni e invarianti dell'oggetto nel codice.Code contracts provide a way to specify preconditions, postconditions, and object invariants in your code. Le precondizioni sono requisiti da soddisfare quando si accede a un metodo o a una proprietà.Preconditions are requirements that must be met when entering a method or property. Le postcondizioni descrivono le aspettative al momento dell'uscita dal codice del metodo o della proprietà.Postconditions describe expectations at the time the method or property code exits. Le invarianti dell'oggetto descrivono lo stato previsto per una classe in stato integro.Object invariants describe the expected state for a class that is in a good state.

I contratti di codice includono classi che consentono di contrassegnare il codice, un analizzatore statico per l'analisi in fase di compilazione e un analizzatore di runtime.Code contracts include classes for marking your code, a static analyzer for compile-time analysis, and a runtime analyzer. Le classi per i contratti di codice sono disponibili nello spazio dei nomi System.Diagnostics.Contracts.The classes for code contracts can be found in the System.Diagnostics.Contracts namespace.

I vantaggi dei contratti di codice includono:The benefits of code contracts include the following:

  • Test migliorati: i contratti di codice consentono la verifica statica, il controllo di runtime e la generazione di documentazione.Improved testing: Code contracts provide static contract verification, runtime checking, and documentation generation.

  • Strumenti di test automatici: è possibile usare i contratti di codice per generare unit test più significativi eliminando gli argomenti di test inutili che non soddisfano le precondizioni.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.

  • Verifica statica: lo strumento di controllo statico può rilevare eventuali violazioni dei contratti senza eseguire il programma.Static verification: The static checker can decide whether there are any contract violations without running the program. Verifica la presenza di contratti impliciti, ad esempio dereferenziazioni null e limiti di matrici, e di contratti espliciti.It checks for implicit contracts, such as null dereferences and array bounds, and explicit contracts.

  • Documentazione di riferimento: il generatore di documentazione integra i file di documentazione XML esistenti con le informazioni sul contratto.Reference documentation: The documentation generator augments existing XML documentation files with contract information. Sono anche presenti fogli di stile utilizzabili con Sandcastle in modo che nelle pagine della documentazione generate siano contenute sezioni relative ai contratti.There are also style sheets that can be used with Sandcastle so that the generated documentation pages have contract sections.

I contratti possono essere usati immediatamente da tutti i linguaggi di .NET Framework; non è necessario scrivere un parser o un compilatore speciale.All .NET Framework languages can immediately take advantage of contracts; you do not have to write a special parser or compiler. Un componente aggiuntivo di Visual Studio consente di specificare il livello di analisi dei contratti di codice da eseguire.A Visual Studio add-in lets you specify the level of code contract analysis to be performed. Gli analizzatori possono confermare che i contratti sono formalmente corretti (controllo del tipo e risoluzione dei nomi) e possono produrre un form compilato dei contratti nel formato 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 funzionalità di creazione dei contratti in Visual Studio consente di usare IntelliSense standard fornito dallo strumento.Authoring contracts in Visual Studio lets you take advantage of the standard IntelliSense provided by the tool.

La maggior parte dei metodi nella classe dei contratti sono compilati in modo condizionale; in altre parole, il compilatore genera chiamate a questi metodi solo quando si definisce un simbolo speciale, CONTRACTS_FULL, tramite la direttiva #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. CONTRACTS_FULL consente di scrivere contratti nel codice senza usare le direttive #ifdef; è possibile produrre build diverse, alcune con contratti e altre senza.CONTRACTS_FULL lets you write contracts in your code without using #ifdef directives; you can produce different builds, some with contracts, and some without.

Per gli strumenti e le istruzioni dettagliate per l'uso dei contratti di codice, vedere Code Contracts(Contratti di codice) nel sito Web MSDN DevLabs.For tools and detailed instructions for using code contracts, see Code Contracts on the MSDN DevLabs Web site.

PreconditionsPreconditions

È possibile esprimere delle precondizioni usando il metodo Contract.Requires.You can express preconditions by using the Contract.Requires method. Le precondizioni specificano lo stato nel momento in cui viene richiamato un metodo.Preconditions specify state when a method is invoked. In genere, vengono usate per specificare valori di parametro validi.They are generally used to specify valid parameter values. Tutti i membri menzionati nelle precondizioni devono essere accessibili almeno quanto il metodo stesso; in caso contrario, la precondizione potrebbe non essere compresa da tutti i chiamanti di un metodo.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 condizione non deve avere effetti collaterali.The condition must have no side-effects. Il comportamento in fase di esecuzione delle precondizioni con errori è determinato dall'analizzatore di runtime.The run-time behavior of failed preconditions is determined by the runtime analyzer.

Ad esempio, la precondizione seguente indica che il parametro x non deve essere null.For example, the following precondition expresses that parameter x must be non-null.

Contract.Requires( x != null );

Se il codice deve generare una particolare eccezione in caso di errore di una precondizione, è possibile usare l'overload generico di Requires come descritto di seguito.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" );

Istruzioni Requires legacyLegacy Requires Statements

La maggior parte del codice contiene la convalida dei parametri sotto forma di codice if-then-throw.Most code contains some parameter validation in the form of if-then-throw code. Gli strumenti dei contratti riconoscono queste istruzioni come precondizioni nei casi seguenti:The contract tools recognize these statements as preconditions in the following cases:

Quando le istruzioni if-then-throw vengono visualizzate in questo formato, gli strumenti le riconoscono come istruzioni requires legacy.When if-then-throw statements appear in this form, the tools recognize them as legacy requires statements. Se la sequenza if-then-throw non è seguita da altri contratti, terminare il codice con il metodo 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  

La condizione nel test precedente è una precondizione negata.Note that the condition in the preceding test is a negated precondition. La precondizione effettiva sarebbe x != null. Una precondizione negata è altamente limitata: deve essere scritta come mostrato nell'esempio precedente, quindi non deve contenere clausole else e il corpo della clausola then deve essere un'unica istruzione 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. Il test if è soggetto a regole di purezza e visibilità (vedere Linee guida di utilizzo), ma l'espressione throw è soggetta solo a regole di purezza.The if test is subject to both purity and visibility rules (see Usage Guidelines), but the throw expression is subject only to purity rules. Tuttavia, il tipo dell'eccezione generata deve essere visibile quanto il metodo in cui si verifica il contratto.However, the type of the exception thrown must be as visible as the method in which the contract occurs.

PostconditionsPostconditions

Le postcondizioni sono contratti per lo stato di un metodo nel momento in cui termina.Postconditions are contracts for the state of a method when it terminates. La postcondizione viene controllata appena prima dell'uscita da un metodo.The postcondition is checked just before exiting a method. Il comportamento in fase di esecuzione delle postcondizioni con errori viene determinato dall'analizzatore di runtime.The run-time behavior of failed postconditions is determined by the runtime analyzer.

Diversamente dalle precondizioni, le postcondizioni possono fare riferimento a membri con visibilità inferiore.Unlike preconditions, postconditions may reference members with less visibility. Un client potrebbe non essere in grado di comprendere o usare alcune delle informazioni espresse da una postcondizione tramite uno stato privato, tuttavia ciò non influisce sulla capacità del client di usare il metodo correttamente.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.

Postcondizioni standardStandard Postconditions

È possibile esprimere postcondizioni standard con il metodo Ensures.You can express standard postconditions by using the Ensures method. Le postcondizioni esprimono una condizione che deve essere true quando il metodo termina regolarmente.Postconditions express a condition that must be true upon normal termination of the method.

Contract.Ensures( this.F > 0 );

Postcondizioni eccezionaliExceptional Postconditions

Le postcondizioni eccezionali sono postcondizioni che devono essere true quando una particolare eccezione viene generata da un metodo.Exceptional postconditions are postconditions that should be true when a particular exception is thrown by a method. È possibile specificare queste postcondizioni tramite il metodo Contract.EnsuresOnThrow, come mostrato nell'esempio seguente.You can specify these postconditions by using the Contract.EnsuresOnThrow method, as the following example shows.

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

L'argomento è la condizione che deve essere true quando viene generata un'eccezione che corrisponde a un sottotipo di T.The argument is the condition that must be true whenever an exception that is a subtype of T is thrown.

Alcuni tipi di eccezione sono difficili da usare in una postcondizione eccezionale.There are some exception types that are difficult to use in an exceptional postcondition. Ad esempio, l'uso del tipo Exception per T richiede che il metodo garantisca la condizione indipendentemente dal tipo di eccezione generato, anche se si tratta di un overflow dello stack o di un'altra eccezione impossibile da controllare.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. Le postcondizioni eccezionali devono essere usate solo per eccezioni specifiche che potrebbero essere generate quando viene chiamato un membro, ad esempio quando viene generata un'eccezione InvalidTimeZoneException per una chiamata al metodo 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.

Postcondizioni specialiSpecial Postconditions

I seguenti metodi possono essere usati solo all'interno di postcondizioni:The following methods may be used only within postconditions:

  • È possibile fare riferimento ai valori restituiti dai metodi nelle postcondizioni usando l'espressione Contract.Result<T>(), dove T viene sostituito dal tipo restituito del metodo.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. Quando il compilatore non è in grado di dedurre il tipo, è necessario fornirlo in modo esplicito.When the compiler is unable to infer the type, you must explicitly provide it. Il compilatore C#, ad esempio, non è in grado di dedurre i tipi per i metodi che non accettano argomenti, pertanto richiede la seguente postcondizione: Contract.Ensures(0 <Contract.Result<int>()). I metodi con un tipo restituito void non possono fare riferimento a Contract.Result<T>() nelle relative postcondizioni.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.

  • Un valore di prestato in una postcondizione fa riferimento al valore di un'espressione all'inizio di un metodo o di una proprietà.A prestate value in a postcondition refers to the value of an expression at the start of a method or property. Usa l'espressione Contract.OldValue<T>(e), dove T è il tipo di e.It uses the expression Contract.OldValue<T>(e), where T is the type of e. È possibile omettere l'argomento di tipo generico quando il compilatore è in grado di dedurre il tipo.You can omit the generic type argument whenever the compiler is able to infer its type. Il compilatore C#, ad esempio, deduce sempre il tipo poiché accetta un argomento. Esistono diverse restrizioni relative a quanto può accadere in e e i contesti nei quali può essere visualizzata un'espressione Old.(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. Un'espressione Old non può contenere un'altra espressione Old.An old expression cannot contain another old expression. In particolare, un'espressione Old deve fare riferimento a un valore esistente nello stato di precondizione del metodo.Most importantly, an old expression must refer to a value that existed in the method's precondition state. In altre parole, deve essere un'espressione valutabile finché la precondizione del metodo resta true.In other words, it must be an expression that can be evaluated as long as the method's precondition is true. Di seguito sono riportate diverse istanze di questa regola.Here are several instances of that rule.

    • Il valore deve esistere nello stato di precondizione del metodo.The value must exist in the method's precondition state. Per fare riferimento a un campo in un oggetto, le precondizioni devono garantire che tale oggetto sia sempre non null.In order to reference a field on an object, the preconditions must guarantee that that object is always non-null.

    • Non è possibile fare riferimento al valore restituito del metodo in un'espressione Old:You cannot refer to the method's return value in an old expression:

      Contract.OldValue(Contract.Result<int>() + x) // ERROR  
      
    • Non è possibile fare riferimento a parametri out in un'espressione Old.You cannot refer to out parameters in an old expression.

    • Un'espressione Old non può dipendere dalla variabile associata di un quantificatore se l'intervallo del quantificatore dipende dal valore restituito del metodo: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  
      
    • Un'espressione Old non può fare riferimento al parametro del delegato anonimo in una chiamata a ForAll o Exists a meno che non venga usata come indicizzatore o argomento di una chiamata al metodo: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  
      
    • Un'espressione Old non può verificarsi nel corpo di un delegato anonimo se il valore dell'espressione dipende da uno dei parametri del delegato, a meno che quest'ultimo non sia un argomento del metodo ForAll o 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  
      
    • I parametri Out presentano un problema in quanto i contratti vengono visualizzati prima del corpo del metodo e la maggior parte dei compilatori non consente riferimenti ai parametri out nelle postcondizioni.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. Per risolvere il problema, la classe Contract fornisce il metodo ValueAtReturn che consente una postcondizione basata su un parametro 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;  
      

      Come per il metodo OldValue, è possibile omettere il parametro di tipo generico quando il compilatore è in grado di dedurre il tipo.As with the OldValue method, you can omit the generic type parameter whenever the compiler is able to infer its type. Il rewriter del contratto sostituisce la chiamata al metodo con il valore del parametro out.The contract rewriter replaces the method call with the value of the out parameter. Il metodo ValueAtReturn può essere visualizzato solo nelle postcondizioni.The ValueAtReturn method may appear only in postconditions. L'argomento del metodo deve essere un parametro out o un campo del parametro out di una struttura.The argument to the method must be an out parameter or a field of a structure out parameter. Quest'ultimo è utile anche in caso di riferimento a campi nella postcondizione di un costruttore della struttura.The latter is also useful when referring to fields in the postcondition of a structure constructor.

      Nota

      Attualmente, gli strumenti di analisi dei contratti di codice non verificano se i parametri out vengono inizializzati correttamente e ne ignorano la menzione nella postcondizione.Currently, the code contract analysis tools do not check whether out parameters are initialized properly and disregard their mention in the postcondition. Quindi, nell'esempio precedente, se la riga dopo il contratto avesse usato il valore x anziché assegnare un numero intero, un compilatore non avrebbe generato l'errore corretto.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. Tuttavia, in una build in cui il simbolo del preprocessore CONTRACTS_FULL non viene definito (ad esempio in una build di rilascio), il compilatore genererà un errore.However, on a build where the CONTRACTS_FULL preprocessor symbol is not defined (such asa release build), the compiler will issue an error.

InvariantiInvariants

Le invarianti dell'oggetto sono condizioni che devono essere true per ogni istanza di una classe quando l'oggetto è visibile a un client.Object invariants are conditions that should be true for each instance of a class whenever that object is visible to a client. Esprimono le condizioni con le quali l'oggetto viene considerato corretto.They express the conditions under which the object is considered to be correct.

I metodi invarianti vengono contrassegnati ai fini dell'identificazione con l'attributo ContractInvariantMethodAttribute.The invariant methods are identified by being marked with the ContractInvariantMethodAttribute attribute. I metodi invarianti non devono contenere codice, fatta eccezione per una sequenza di chiamate al metodo Invariant, ognuna delle quali specifica una singola invariante, come mostrato nell'esempio seguente.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);  
...  
}  

Le invarianti vengono definite in modo condizionale dal simbolo del preprocessore CONTRACTS_FULL.Invariants are conditionally defined by the CONTRACTS_FULL preprocessor symbol. Durante il controllo in fase di esecuzione, le invarianti vengono controllate alla fine di ogni metodo pubblico.During run-time checking, invariants are checked at the end of each public method. Se un'invariante menziona un metodo pubblico nella stessa classe, il controllo dell'invariante che avverrebbe normalmente alla fine di tale metodo viene disabilitato.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. Al contrario, il controllo viene eseguito solo alla fine della chiamata al metodo più esterna in quella classe.Instead, the check occurs only at the end of the outermost method call to that class. Ciò avviene anche se la classe viene immessa di nuovo a causa di una chiamata a un metodo in un'altra classe.This also happens if the class is re-entered because of a call to a method on another class. L'eventuale presenza di finalizzatori di oggetti o di metodi che implementano il metodo Dispose non viene verificata nelle invarianti.Invariants are not checked for object finalizers or for any methods that implement the Dispose method.

Linee guida di utilizzoUsage Guidelines

Ordine dei contrattiContract Ordering

La tabella seguente mostra l'ordine degli elementi da usare per la scrittura di contratti del metodo.The following table shows the order of elements you should use when you write method contracts.

If-then-throw statements Precondizioni pubbliche compatibili con le versioni precedentiBackward-compatible public preconditions
Requires Tutte le precondizioni pubbliche.All public preconditions.
Ensures Tutte le postcondizioni pubbliche (normali).All public (normal) postconditions.
EnsuresOnThrow Tutte le postcondizioni pubbliche eccezionali.All public exceptional postconditions.
Ensures Tutte le postcondizioni private/interne (normali).All private/internal (normal) postconditions.
EnsuresOnThrow Tutte le postcondizioni private/interne eccezionali.All private/internal exceptional postconditions.
EndContractBlock Se si usano le precondizioni di stile if-then-throw senza altri contratti, inserire una chiamata a EndContractBlock per indicare che tutti i controlli if precedenti sono precondizioni.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.

PurezzaPurity

Tutti i metodi chiamati all'interno di un contratto devono essere puri; in altre parole, non devono aggiornare stati preesistenti.All methods that are called within a contract must be pure; that is, they must not update any preexisting state. Un metodo puro può modificare gli oggetti creati in seguito all'accesso al metodo stesso.A pure method is allowed to modify objects that have been created after entry into the pure method.

Gli strumenti dei contratti di codice presuppongono che i seguenti elementi di codice siano puri:Code contract tools currently assume that the following code elements are pure:

  • Metodi contrassegnati con PureAttribute.Methods that are marked with the PureAttribute.

  • Tipi contrassegnati con PureAttribute (l'attributo si applica a tutti i metodi del tipo).Types that are marked with the PureAttribute (the attribute applies to all the type's methods).

  • Funzioni di accesso get della proprietà.Property get accessors.

  • Operatori (metodi statici i cui nomi iniziano con "op" e che hanno uno o due parametri e un tipo restituito non void).Operators (static methods whose names start with "op", and that have one or two parameters and a non-void return type).

  • Tutti i metodi il cui nome completo inizia con "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" o "System.Type".Any method whose fully qualified name begins with "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path", or "System.Type".

  • Tutti i delegati richiamati, purché al tipo del delegato venga attribuito PureAttribute.Any invoked delegate, provided that the delegate type itself is attributed with the PureAttribute. I tipi del delegato System.Predicate<T> e System.Comparison<T> sono considerati puri.The delegate types System.Predicate<T> and System.Comparison<T> are considered pure.

VisibilitàVisibility

Tutti i membri menzionati in un contratto devono essere visibili almeno quanto il metodo in cui vengono visualizzati. All members mentioned in a contract must be at least as visible as the method in which they appear. Un campo privato, ad esempio, non può essere menzionato in una precondizione per un metodo pubblico; i client non possono convalidare un simile contratto prima di chiamare il metodo.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. Tuttavia, se il campo è contrassegnato con ContractPublicPropertyNameAttribute, è esente da queste regole.However, if the field is marked with the ContractPublicPropertyNameAttribute, it is exempt from these rules.

EsempioExample

L'esempio seguente mostra l'uso dei contratti di codice.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