Contratti di codice (.NET Framework)

  • Articolo

I contratti di codice consentono di specificare precondizioni, postcondizioni e invarianti dell'oggetto nel codice .NET Framework. Le precondizioni sono requisiti da soddisfare quando si accede a un metodo o a una proprietà. Le postcondizioni descrivono le aspettative al momento dell'uscita dal codice del metodo o della proprietà. Le invarianti dell'oggetto descrivono lo stato previsto per una classe in stato integro.

Nota

I contratti di codice non sono supportati in .NET 5+ (incluse le versioni di .NET Core). Valutare la possibilità di usare tipi riferimento nullable in alternativa.

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. Le classi per i contratti di codice sono disponibili nello spazio dei nomi System.Diagnostics.Contracts.

I vantaggi dei contratti di codice includono:

  • Test migliorati: i contratti di codice consentono la verifica statica, il controllo di runtime e la generazione di documentazione.

  • 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.

  • Verifica statica: lo strumento di controllo statico può rilevare eventuali violazioni dei contratti senza eseguire il programma. Verifica la presenza di contratti impliciti, ad esempio dereferenziazioni null e limiti di matrici, e di contratti espliciti.

  • Documentazione di riferimento: il generatore di documentazione integra i file di documentazione XML esistenti con le informazioni sul contratto. Sono anche presenti fogli di stile utilizzabili con Sandcastle in modo che nelle pagine della documentazione generate siano contenute sezioni relative ai contratti.

I contratti possono essere usati immediatamente da tutti i linguaggi di .NET Framework; non è necessario scrivere un parser o un compilatore speciale. Un componente aggiuntivo di Visual Studio consente di specificare il livello di analisi dei contratti di codice da eseguire. 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). La funzionalità di creazione dei contratti in Visual Studio consente di usare IntelliSense standard fornito dallo strumento.

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. CONTRACTS_FULL consente di scrivere contratti nel codice senza usare le direttive #ifdef; è possibile produrre build diverse, alcune con contratti e altre senza.

Per gli strumenti e le istruzioni dettagliate per l'uso dei contratti di codice, vedere Contratti di codice nel sito del marketplace di Visual Studio.

Condizioni preliminari

È possibile esprimere delle precondizioni usando il metodo Contract.Requires. Le precondizioni specificano lo stato nel momento in cui viene richiamato un metodo. In genere, vengono usate per specificare valori di parametro validi. 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. La condizione non deve avere effetti collaterali. Il comportamento in fase di esecuzione delle precondizioni con errori è determinato dall'analizzatore di runtime.

Ad esempio, la precondizione seguente indica che il parametro x non deve essere 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.

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

Istruzioni Requires legacy

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

Quando le istruzioni if-then-throw vengono visualizzate in questo formato, gli strumenti le riconoscono come istruzioni requires legacy. Se la sequenza if-then-throw non è seguita da altri contratti, terminare il codice con il metodo Contract.EndContractBlock.

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

La condizione nel test precedente è una precondizione negata. 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. 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. Tuttavia, il tipo dell'eccezione generata deve essere visibile quanto il metodo in cui si verifica il contratto.

Postconditions

Le postcondizioni sono contratti per lo stato di un metodo nel momento in cui termina. La postcondizione viene controllata appena prima dell'uscita da un metodo. Il comportamento in fase di esecuzione delle postcondizioni con errori viene determinato dall'analizzatore di runtime.

Diversamente dalle precondizioni, le postcondizioni possono fare riferimento a membri con visibilità inferiore. 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.

Postcondizioni standard

È possibile esprimere postcondizioni standard con il metodo Ensures. Le postcondizioni esprimono una condizione che deve essere true quando il metodo termina regolarmente.

Contract.Ensures(this.F > 0);

Postcondizioni eccezionali

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

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.

Alcuni tipi di eccezione sono difficili da usare in una postcondizione eccezionale. 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. 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.

Postcondizioni speciali

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

  • È 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. Quando il compilatore non è in grado di dedurre il tipo, è necessario fornirlo in modo esplicito. 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.

  • Un valore di prestato 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 quando il compilatore è in grado di dedurre il tipo. 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. Un'espressione Old non può contenere un'altra espressione Old. In particolare, un'espressione Old deve fare riferimento a un valore esistente nello stato di precondizione del metodo. In altre parole, deve essere un'espressione valutabile finché la precondizione del metodo resta true. Di seguito sono riportate diverse istanze di questa regola.

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

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

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

    • Non è possibile fare riferimento a parametri out in un'espressione Old.

    • Un'espressione Old 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 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:

      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:

      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. Per risolvere il problema, la classe Contract fornisce il metodo ValueAtReturn che consente una postcondizione basata su un parametro out.

      public void OutParam(out int x)
{
    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. Il rewriter del contratto sostituisce la chiamata al metodo con il valore del parametro out. Il metodo ValueAtReturn può essere visualizzato solo nelle postcondizioni. L'argomento del metodo deve essere un parametro out o un campo del parametro out di una struttura. Quest'ultimo è utile anche in caso di riferimento a campi nella postcondizione di un costruttore della struttura.

      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. 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. 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.

Invarianti

Le invarianti dell'oggetto sono condizioni che devono essere true per ogni istanza di una classe quando l'oggetto è visibile a un client. Esprimono le condizioni con le quali l'oggetto viene considerato corretto.

I metodi invarianti vengono contrassegnati ai fini dell'identificazione con l'attributo ContractInvariantMethodAttribute. 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.

[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. Durante il controllo in fase di esecuzione, le invarianti vengono controllate alla fine di ogni metodo pubblico. Se un'invariante menziona un metodo pubblico nella stessa classe, il controllo dell'invariante che avverrebbe normalmente alla fine di tale metodo viene disabilitato. Al contrario, il controllo viene eseguito solo alla fine della chiamata al metodo più esterna in quella classe. Ciò avviene anche se la classe viene immessa di nuovo 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 di IDisposable.Dispose.

Linee guida per l'utilizzo

Ordine dei contratti

La tabella seguente mostra l'ordine degli elementi da usare per la scrittura di contratti del metodo.

If-then-throw statements Precondizioni pubbliche compatibili con le versioni precedenti
Requires Tutte le precondizioni pubbliche.
Ensures Tutte le postcondizioni pubbliche (normali).
EnsuresOnThrow Tutte le postcondizioni pubbliche eccezionali.
Ensures Tutte le postcondizioni private/interne (normali).
EnsuresOnThrow Tutte le postcondizioni private/interne eccezionali.
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.

Purezza

Tutti i metodi chiamati all'interno di un contratto devono essere puri; in altre parole, non devono aggiornare stati preesistenti. Un metodo puro può modificare gli oggetti creati in seguito all'accesso al metodo stesso.

Gli strumenti dei contratti di codice presuppongono che i seguenti elementi di codice siano puri:

  • Metodi contrassegnati con PureAttribute.

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

  • Funzioni di accesso get della proprietà.

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

  • Tutti i metodi il cui nome completo inizia con "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" o "System.Type".

  • Tutti i delegati richiamati, purché al tipo del delegato venga attribuito PureAttribute. I tipi del delegato System.Predicate<T> e System.Comparison<T> sono considerati puri.

Visibilità

Tutti i membri menzionati in un contratto devono essere visibili almeno quanto il metodo in cui vengono visualizzati. 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. Tuttavia, se il campo è contrassegnato con ContractPublicPropertyNameAttribute, è esente da queste regole.

Esempio

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