Condividi tramite

Contratti di codice (.NET Framework)

Annotazioni

Questo articolo è specifico di .NET Framework. Non si applica alle implementazioni più recenti di .NET, incluse .NET 6 e versioni successive.

I contratti di codice consentono di specificare precondizioni, postcondizioni e invarianti di oggetti nel codice .NET Framework. Le precondizioni sono i requisiti che devono essere soddisfatti per utilizzare un metodo o una proprietà. Le postcondizioni descrivono le aspettative al momento in cui il metodo o il codice proprietà esce. Le invarianti dell'oggetto descrivono lo stato previsto per una classe in uno stato valido.

Annotazioni

I contratti di codice non sono supportati in .NET 5+ (incluse le versioni di .NET Core). Considera l'uso di tipi di riferimento Nullable invece.

I contratti di codice includono classi per contrassegnare il codice, un analizzatore statico per l'analisi in fase di compilazione e un analizzatore di runtime. Le classi per i contratti di codice sono disponibili nel namespace System.Diagnostics.Contracts.

I vantaggi dei contratti di codice includono quanto segue:

  • Test migliorati: i contratti di codice forniscono la verifica statica del contratto, il controllo di runtime e la generazione della documentazione.

  • Strumenti di test automatici: è possibile usare contratti di codice per generare unit test più significativi filtrando argomenti di test senza significato che non soddisfano le precondizioni.

  • Verifica statica: il controllo statico può decidere se sono presenti violazioni del contratto senza eseguire il programma. Verifica la presenza di contratti impliciti, ad esempio dereferenziazioni Null e limiti di matrice e contratti espliciti.

  • Documentazione di riferimento: il generatore di documentazione aumenta i file di documentazione XML esistenti con informazioni sul contratto. Esistono anche fogli di stile che possono essere usati con Sandcastle in modo che le pagine della documentazione generate abbiano sezioni di contratto.

Tutti i linguaggi .NET Framework possono sfruttare immediatamente i contratti; non è necessario scrivere un parser o un compilatore speciale. Un componente aggiuntivo di Visual Studio consente di specificare il livello di analisi del contratto di codice da eseguire. Gli analizzatori possono verificare che i contratti siano ben formati (controllo dei tipi e risoluzione dei nomi) e possano produrre una forma compilata dei contratti in formato CIL (Common Intermediate Language). La creazione di contratti in Visual Studio consente di sfruttare il vantaggio dell'IntelliSense standard fornito dal programma.

La maggior parte dei metodi nella classe del contratto viene compilata in modo condizionale; ovvero, il compilatore genera chiamate a questi metodi solo quando si definisce un simbolo speciale, CONTRACTS_FULL, usando la #define direttiva . CONTRACTS_FULL consente di scrivere contratti nel codice senza usare #ifdef direttive; è possibile produrre compilazioni diverse, alcuni con contratti e alcuni senza.

Per gli strumenti e istruzioni dettagliate sull'uso dei contratti di codice, vedere Contratti di codice nel sito di Visual Studio Marketplace.

Condizioni

È possibile esprimere le precondizioni usando il Contract.Requires metodo . Le precondizioni specificano lo stato quando viene richiamato un metodo. Vengono in genere usati per specificare valori di parametro validi. Tutti i membri menzionati nelle precondizioni devono essere almeno accessibili come il metodo stesso; in caso contrario, la precondizione potrebbe non essere compresa da tutti i chiamanti di un metodo. La condizione non deve avere effetti collaterali. Il comportamento di runtime delle precondizioni non riuscite è determinato dall'analizzatore del tempo di esecuzione.

Ad esempio, la precondizione seguente esprime che il parametro x deve essere diverso da null.

Contract.Requires(x != null);

Se il codice deve generare una particolare eccezione in caso di errore di una precondizione, è possibile utilizzare l'overload generico di Requires nel modo seguente.

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

Istruzioni Richieste Legacy

La maggior parte del codice contiene una convalida dei parametri sotto forma di if-then-throw codice. Gli strumenti del contratto riconoscono queste istruzioni come precondizioni nei casi seguenti:

  • Le istruzioni vengono visualizzate prima di qualsiasi altra istruzione in un metodo.

  • L'intero set di istruzioni di questo tipo è seguito da una chiamata esplicita al metodo Contract, ad esempio una chiamata al metodo Requires, Ensures, EnsuresOnThrow o EndContractBlock.

Quando if-then-throw le istruzioni vengono visualizzate in questo formato, gli strumenti li riconoscono come istruzioni legacy.requires Se nessun altro contratto segue la if-then-throw sequenza, terminare il codice con il Contract.EndContractBlock metodo .

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

Si noti che la condizione nel test precedente è una precondizione negata. (La precondizione effettiva sarebbe x != null.) Una precondizione negata è altamente limitata: deve essere scritta come illustrato nell'esempio precedente; ovvero non deve contenere clausole else, e il corpo della clausola then deve essere un singolo comando throw. Il if test è soggetto a regole di purezza e visibilità (vedere Linee guida sull'utilizzo), ma l'espressione throw è soggetta solo alle regole di purezza. Tuttavia, il tipo di eccezione sollevata deve essere visibile quanto il metodo in cui avviene il contratto.

Postcondizioni

Le postcondizioni sono contratti riguardanti lo stato di un metodo quando termina. La postcondizione viene verificata subito prima di uscire da un metodo. Il comportamento al momento dell'esecuzione delle postcondizioni non riuscite è determinato dall'analizzatore del tempo di esecuzione.

A differenza delle precondizioni, le postcondizioni possono fare riferimento a membri con una minore visibilità. Un client potrebbe non essere in grado di comprendere o usare alcune delle informazioni espresse da una postcondizione usando lo stato privato, ma ciò non influisce sulla capacità del client di usare correttamente il metodo.

Postcondizioni standard

È possibile esprimere postcondizioni standard usando il Ensures metodo . Le postcondizioni esprimono una condizione che deve essere true al termine normale del metodo.

Contract.Ensures(this.F > 0);

Postcondizioni straordinarie

Le postcondizioni eccezionali sono postcondizioni che devono essere true quando viene generata una particolare eccezione da un metodo. È possibile specificare queste postcondizioni usando il Contract.EnsuresOnThrow metodo , come illustrato nell'esempio seguente.

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

L'argomento è la condizione che deve essere true ogni volta che viene generata un'eccezione che è un sottotipo di T .

Esistono alcuni tipi di eccezione difficili da usare in una postcondizione eccezionale. Ad esempio, l'uso del tipo Exception per T richiede al metodo di garantire la condizione indipendentemente dal tipo di eccezione generata, anche se si tratta di un overflow dello stack o di un'altra eccezione impossibile da controllare. È opportuno usare postcondizioni straordinarie solo per particolari eccezioni che potrebbero essere sollevate quando viene chiamato un membro, ad esempio quando viene sollevata un'eccezione InvalidTimeZoneException per una chiamata al metodo TimeZoneInfo.

Postcondizioni speciali

I metodi seguenti possono essere usati solo all'interno di postcondizioni:

  • È possibile fare riferimento ai valori restituiti dal metodo in postcondizioni usando l'espressione Contract.Result<T>(), dove T viene sostituito dal tipo restituito del metodo . Quando il compilatore non è in grado di dedurre il tipo, è necessario specificarlo in modo esplicito. Ad esempio, il compilatore C# non è in grado di dedurre i tipi per i metodi che non accettano argomenti, quindi richiede la postcondizione seguente: Contract.Ensures(0 <Contract.Result<int>()) i metodi con un tipo restituito di void non possono fare riferimento Contract.Result<T>() nelle rispettive postcondizioni.

  • Un valore di pre-esecuzione in una postcondizione fa riferimento al valore di un'espressione all'inizio di un metodo o di una proprietà. Usa l'espressione Contract.OldValue<T>(e), dove T è il tipo di e. È possibile omettere l'argomento di tipo generico ogni volta che il compilatore è in grado di dedurre il relativo tipo. Ad esempio, il compilatore C# deduce sempre il tipo perché accetta un argomento. Esistono diverse restrizioni su ciò che può verificarsi in e e sui contesti in cui può essere visualizzata un'espressione precedente. Un'espressione precedente non può contenere un'altra espressione precedente. Soprattutto, un'espressione precedente deve fare riferimento a un valore esistente nello stato di precondizione del metodo. In altre parole, deve essere un'espressione che può essere valutata purché la precondizione del metodo sia true. Di seguito sono riportate diverse istanze di tale regola.

    • Il valore deve esistere nello stato di precondizione del metodo. Per fare riferimento a un campo su un oggetto, le precondizioni devono garantire che l'oggetto sia sempre diverso da Null.

    • Non è possibile fare riferimento al valore restituito del metodo in un'espressione precedente:

      Contract.OldValue(Contract.Result<int>() + x) // ERROR

    • Non è possibile fare riferimento ai out parametri in un'espressione precedente.

    • Un'espressione precedente non può dipendere dalla variabile associata di un quantificatore se l'intervallo del quantificatore dipende dal valore restituito del metodo:

      Contract.ForAll(0, Contract.Result<int>(), i => Contract.OldValue(xs[i]) > 3); // ERROR

    • Un'espressione vecchia non può fare riferimento al parametro del delegato senza nome in una ForAll o chiamata Exists a meno che non venga usata come indicizzatore o argomento di una chiamata al metodo.

      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 vecchia non può verificarsi nel corpo di un delegato anonimo se il valore dell'espressione vecchia dipende da uno dei parametri del delegato anonimo, a meno che il delegato anonimo non sia un argomento ai metodi ForAll o Exists.

      Method(... (T t) => Contract.OldValue(... t ...) ...); // ERROR

    • Out I parametri presentano un problema perché i contratti vengono visualizzati prima del corpo del metodo e la maggior parte dei compilatori non consente riferimenti ai out parametri nelle postcondizioni. Per risolvere questo problema, la Contract classe fornisce il ValueAtReturn metodo , che consente una postcondizione basata su un out parametro.

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

      Come con il OldValue metodo , è possibile omettere il parametro di tipo generico ogni volta che il compilatore è in grado di dedurre il relativo tipo. Il rewriter del contratto sostituisce la chiamata al metodo con il valore del parametro out. Il ValueAtReturn metodo può comparire solo nelle postcondizioni. L'argomento del metodo deve essere un out parametro o un campo di un parametro di struttura out . Quest'ultimo è utile anche quando si fa riferimento a campi nella postcondizione di un costruttore di struttura.

      Annotazioni

      Attualmente, gli strumenti di analisi del contratto di codice non controllano se out i parametri vengono inizializzati correttamente e ignorano la loro menzione nella postcondizione. Pertanto, nell'esempio precedente, se la riga dopo il contratto aveva usato il valore di x anziché assegnarvi un numero intero, un compilatore non genera l'errore corretto. Tuttavia, in una compilazione in cui il simbolo del preprocessore CONTRACTS_FULL non è definito ,ad esempio una build di rilascio, il compilatore genererà un errore.

Invarianti

Le invarianti dell'oggetto sono condizioni che devono essere vere per ogni istanza di una classe ogni volta che tale oggetto è visibile a un client. Esprimono le condizioni in base alle quali l'oggetto viene considerato corretto.

I metodi invarianti vengono identificati contrassegnati con l'attributo ContractInvariantMethodAttribute . I metodi invarianti non devono contenere codice tranne una sequenza di chiamate al Invariant metodo , ognuna delle quali specifica un singolo invariante, come illustrato nell'esempio seguente.

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

Gli invarianti vengono definiti in modo condizionale dal simbolo del preprocessore CONTRACTS_FULL. Durante il controllo di runtime, le invarianti vengono controllate alla fine di ogni metodo pubblico. Se un invariante menziona un metodo pubblico nella stessa classe, il controllo invariante che normalmente si verifica alla fine di tale metodo pubblico è disabilitato. Al contrario, il controllo si verifica solo alla fine della chiamata al metodo più esterno a tale classe. Ciò si verifica anche se la classe viene nuovamente immessa a causa di una chiamata a un metodo in un'altra classe. Le invarianti non vengono controllate per un finalizzatore di oggetto e un'implementazione IDisposable.Dispose .

Linee guida sull'utilizzo

Ordinamento dei contratti

Nella tabella seguente viene illustrato l'ordine degli elementi da usare quando si scrivono contratti di metodo.

If-then-throw statements Precondizioni pubbliche retrocompatibili
Requires Tutte le precondizioni pubbliche.
Ensures Tutte le postcondizioni pubbliche (standard).
EnsuresOnThrow Tutte le postcondizioni eccezionali pubbliche.
Ensures Tutte le postcondizioni private/interne (normali).
EnsuresOnThrow Tutte le postcondizioni eccezionali private/interne.
EndContractBlock Se si usano if-then-throw precondizioni di stile senza altri contratti, effettuare una chiamata a EndContractBlock per indicare che tutti i controlli precedenti sono precondizioni.

Purezza

Tutti i metodi chiamati all'interno di un contratto devono essere puri; ovvero non devono aggiornare alcuno stato preesistente. È consentito un metodo puro per modificare gli oggetti creati dopo l'immissione nel metodo puro.

Gli strumenti del contratto di codice presuppongono attualmente che gli elementi di codice seguenti siano puri:

  • Metodi contrassegnati con .PureAttribute

  • Tipi contrassegnati con ( PureAttribute l'attributo si applica a tutti i metodi del tipo).

  • Funzioni di accesso get delle proprietà.

  • Operatori (metodi statici i cui nomi iniziano con "op" e che hanno uno o due parametri e che restituiscono un tipo non nullo).

  • Qualsiasi metodo il cui nome completo inizia con "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" o "System.Type".

  • Qualsiasi delegato invocato, a condizione che il tipo delegato stesso sia attribuito con PureAttribute. I tipi delegato System.Predicate<T> e System.Comparison<T> sono considerati puri.

Visibilità

Tutti i membri menzionati in un contratto devono avere una visibilità almeno pari al metodo in cui appaiono. Ad esempio, un campo privato non può essere menzionato in una precondizione per un metodo pubblico; i client non possono convalidare tale contratto prima di chiamare il metodo . Tuttavia, se il campo è contrassegnato con ContractPublicPropertyNameAttribute, è esente da queste regole.

Esempio

Nell'esempio seguente viene illustrato l'uso di contratti di codice.

#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


    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


    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
End Class
  • Last updated on