Contratti di codice

Articolo
08/11/2011

I contratti di codice consentono di specificare precondizioni, postcondizioni e invarianti dell'oggetto nel codice. Le precondizioni sono requisiti da soddisfare quando si accede a un metodo o 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.

I contratti di codice includono classi per il contrassegno del codice, un analizzatore statico per l'analisi in fase di compilazione e un analizzatore di runtime. Le classi per i contratti di codice sono contenute nello spazio dei nomi System.Diagnostics.Contracts.

Tra i vantaggi dei contratti di codice vi sono i seguenti:

Test migliorati: i contratti di codice consentono la verifica statica, il controllo di runtime e la generazione di documentazione.
Strumenti di test automatici: è possibile utilizzare i contratti di codice per generare unit test più significativi eliminando gli argomenti di test inutili che non soddisfano le precondizioni.
Verifica statica: il verificatore statico può stabilire l'eventuale violazione dei contratti senza eseguire il programma. Verifica la presenza di contratti impliciti, ad esempio dereferenziazioni Null e limiti delle matrici, e contratti espliciti.
Documentazione di riferimento: il generatore di documentazione integra i file di documentazione XML esistenti con le informazioni sui contratti. Esistono inoltre fogli di stile che è possibile utilizzare con Sandcastle in modo che le pagine della documentazione generata contengano sezioni relative ai contratti.

I contratti possono essere sfruttati nell'immediato 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 dei tipi e risoluzione dei nomi) e possono produrre una forma compilata dei contratti nel formato MSIL (Microsoft Intermediate Language). La creazione di contratti in Visual Studio consente di sfruttare la versione standard di IntelliSense fornita 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 utilizzare le direttive #ifdef; è possibile produrre compilazioni diverse, alcune con contratti e altre senza.

Per gli strumenti e le istruzioni dettagliate per l'utilizzo dei contratti di codice, vedere Contratti di codice sul sito Web DevLabs di MSDN (la pagina potrebbe essere in inglese).

Preconditions

È possibile esprimere precondizioni utilizzando il metodo Contract.Requires. Le precondizioni specificano lo stato nel momento in cui viene richiamato un metodo. In genere, vengono utilizzate per specificare valori di parametro validi. Tutti i membri menzionati nelle precondizioni devono essere come minimo accessibili 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 deve essere non 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 come segue.

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

Istruzioni Requires legacy

Gran parte del codice include la convalida dei parametri sotto forma di codice if-then-throw. Gli strumenti dei contratti 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 è seguito dalla chiamata a un metodo Contract esplicito, ad esempio una chiamata al metodo Requires, Ensures, EnsuresOnThrow o EndContractBlock.

Quando le istruzioni if-then-throw appaiono in questa forma, 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 illustrato nell'esempio precedente, vale a dire 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 è unicamente soggetta a regole di purezza. Tuttavia, il tipo dell'eccezione generata deve essere visibile quanto il metodo in cui si verifica il contratto.

Postcondizioni

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 è determinato dall'analizzatore di runtime.

Diversamente dalle precondizioni, le postcondizioni possono fare riferimento a membri con visibilità inferiore. È possibile che un client non sia in grado di comprendere o utilizzare alcune delle informazioni espresse da una postcondizione tramite uno stato privato, ma ciò non influisce sulla capacità del client di utilizzare correttamente il metodo.

Postcondizioni standard

È possibile esprimere postcondizioni standard utilizzando 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 utilizzando il metodo Contract.EnsuresOnThrow, come illustrato nell'esempio seguente.

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

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

Alcuni tipi di eccezione sono difficili da utilizzare in una postcondizione eccezionale. Ad esempio, l'utilizzo 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 di controllo impossibile. Le postcondizioni eccezionali devono essere utilizzate 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 utilizzati solo all'interno di postcondizioni:

È possibile fare riferimento ai valori restituiti dai metodi nelle postcondizioni utilizzando 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 uguale a void non possono fare riferimento a Contract. Result<T>() nelle relative postcondizioni.

Un valore pre-stato in una postcondizione fa riferimento al valore di un'espressione all'inizio di un metodo o di una proprietà. Utilizza l'espressione Contract.OldValue<T>(e), dove T è il tipo di e. È possibile omettere l'argomento di tipo generico ogni qualvolta il compilatore è in grado di dedurre il tipo. Il compilatore C#, ad esempio, deduce sempre il tipo poiché accetta un argomento. Esistono diverse restrizioni concernenti 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 tale 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 tale 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 utilizzata 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 un qualsiasi parametro 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<T>, che consente una postcondizione basata su un parametro out.

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

Come per il metodo OldValue<T>, è possibile omettere il parametro di tipo generico ogni qualvolta il compilatore è in grado di dedurre il tipo. Il rewriter dei contratti sostituisce la chiamata al metodo con il valore del parametro out. Il metodo ValueAtReturn<T> 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 ignorano la menzione nella postcondizione.Nell'esempio precedente, pertanto, se la riga dopo il contratto utilizzasse il valore x anziché assegnargli un intero, un compilatore non genererebbe l'errore corretto.Tuttavia, in una compilazione in cui il simbolo del preprocessore CONTRACTS FULL non viene definito (ad esempio una compilazione di rilascio), il compilatore genererà un errore.

Attualmente, gli strumenti di analisi dei contratti di codice non verificano se i parametri out vengono inizializzati correttamente e ignorano la menzione nella postcondizione.Nell'esempio precedente, pertanto, se la riga dopo il contratto utilizzasse il valore x anziché assegnargli un intero, un compilatore non genererebbe l'errore corretto.Tuttavia, in una compilazione in cui il simbolo del preprocessore CONTRACTS FULL non viene definito (ad esempio una compilazione di rilascio), il compilatore genererà un errore.

Condizioni non variabili

Le invarianti dell'oggetto sono condizioni che devono essere true per ogni istanza di una classe ogni qualvolta l'oggetto è visibile a un client. Esprimono le condizioni in cui 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 illustrato 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. Per contro, il controllo viene eseguito solo alla fine della chiamata al metodo più esterna in quella classe. Ciò avviene anche se la classe viene nuovamente immessa a causa di una chiamata a un metodo in un'altra classe. L'eventuale presenza di finalizzatori di oggetti o di metodi che implementano il metodo Dispose non viene verificata nelle invarianti.

Linee guida di utilizzo

Ordine dei contratti

Nella tabella seguente è illustrato l'ordine di elementi da utilizzare 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	In caso di utilizzo di 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 delle proprietà.
Operatori (metodi statici i cui nomi iniziano con "op" e che hanno uno o due parametri e un tipo restituito non void).
Qualsiasi metodo il cui nome completo inizia con "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" o "System.Type".
Qualsiasi delegato richiamato, purché al tipo del delegato stesso 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 come minimo visibili 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

Nell'esempio seguente viene illustrato l'utilizzo dei contratti di codice.

Imports System
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

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);
    }
}

Condividi tramite