Contrats de code

Article
08/10/2011

Les contrats de code offrent un moyen de spécifier des conditions préalables, des post-conditions et des invariants objet dans votre code. Les conditions préalables sont des exigences qui doivent être satisfaites lors de l'entrée d'une méthode ou d'une propriété. Les post-conditions décrivent les attentes au moment de la sortie du code de méthode ou de propriété. Les invariants objet décrivent l'état attendu pour une classe en bon état.

Les contrats de code incluent des classes pour le marquage de votre code, un analyseur statique pour l'analyse au moment de la compilation, ainsi qu'un analyseur au moment de l'exécution. Les classes des contrats de code se trouvent dans l'espace de noms System.Diagnostics.Contracts.

Les avantages des contrats de code sont les suivants :

Tests améliorés : les contrats de code permettent la vérification de contrat statique, la vérification à l'exécution et la génération de documentation.
Outils de test automatiques : vous pouvez utiliser les contrats de code pour générer des tests unitaires plus explicites en filtrant les arguments de test sans signification qui ne satisfont pas les conditions préalables.
Vérification statique : le vérificateur statique peut déterminer s'il existe des violations de contrat sans exécuter le programme. Il recherche des contrats implicites, tels que des déréférences et des limites d'index de tableau nulles, ainsi que des contrats explicites.
Documentation de référence : le générateur de documentation augmente les fichiers de documentation XML existants avec des informations de contrat. Il y a également des feuilles de style qui peuvent être utilisées avec Sandcastle de façon à ce que les pages de documentation générées aient des sections de contrat.

Tous les langages .NET Framework peuvent immédiatement bénéficier de contrats. Vous n'avez pas à écrire un analyseur ou compilateur spécial. Un complément Visual Studio vous permet de spécifier le niveau d'analyse de contrat de code à exécuter. Les analyseurs peuvent confirmer que les contrats sont de forme correcte (vérification de type et résolution de noms) et peuvent produire un formulaire compilé des contrats au format MSIL (Microsoft Intermediate Language). La création de contrats dans Visual Studio vous permet de tirer parti de la fonction IntelliSense standard fournie par l'outil.

La plupart des méthodes dans la classe de contrat sont compilées de façon conditionnelle, à savoir que le compilateur émet des appels à ces méthodes uniquement lorsque vous définissez un symbole spécial, CONTRACTS FULL, à l'aide de la directive #define. CONTRACTS FULL vous permet d'écrire des contrats dans votre code sans utiliser de directives #ifdef ; vous pouvez produire des générations différentes, certaines avec des contrats, d'autres sans.

Pour en savoir plus sur les outils et obtenir des instructions détaillées sur l'utilisation de contrats de code, consultez Contrats de code (page éventuellement en anglais) sur le site Web de MSDN DevLabs.

Preconditions

Vous pouvez exprimer des conditions préalables à l'aide de la méthode Contract.Requires. Les conditions préalables spécifient l'état quand une méthode est appelée. Elles sont généralement utilisées pour indiquer des valeurs de paramètre valides. Tous les membres mentionnés dans les conditions préalables doivent être au moins aussi accessibles que la méthode elle-même. Autrement, la condition préalable peut ne pas être comprise par tous les appelants d'une méthode. La condition ne doit pas avoir d'effets secondaires. Le comportement au moment de l'exécution des conditions préalables non réussies est déterminé par l'analyseur au moment de l'exécution.

Par exemple, la condition préalable suivante indique que le paramètre x doit être non null.

Contract.Requires( x != null );

Si votre code doit lever une exception particulière en cas d'échec d'une condition préalable, vous pouvez utiliser la surcharge générique de Requires comme suit.

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

Instructions Requires héritées

Une grande partie du code contient de la validation de paramètres sous la forme de code if-then-throw. Les outils de contrat reconnaissent ces instructions comme étant des conditions préalables dans les cas suivants :

Ces instructions apparaissent avant les autres dans une méthode.
L'ensemble de ces instructions est suivi d'un appel de méthode Contract explicite, tel qu'un appel à la méthode Requires, Ensures, EnsuresOnThrow ou EndContractBlock.

Lorsque les instructions if-then-throw apparaissent sous cette forme, les outils les reconnaissent en tant qu'instructions requires héritées. Si aucun autre contrat ne suit la séquence if-then-throw, terminez le code par la méthode Contract.EndContractBlock.

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

Notez que la condition du test précédent est une condition préalable négative. (La condition préalable réelle serait x != null.) Une condition préalable négative est très restreinte. Elle doit être écrite comme indiqué dans l'exemple précédent, à savoir qu'elle ne doit pas contenir de clauses else, et le corps de la clause then doit être une instruction throw unique. Le test if est soumis à la fois aux règles de pureté et de visibilité (consultez Indications d'utilisation), mais l'expression throw est uniquement soumise aux règles de pureté. Toutefois, le type de l'exception levée doit être aussi visible que la méthode dans laquelle le contrat se produit.

Postconditions

Les post-conditions sont des contrats pour l'état d'une méthode lorsqu'elle se termine. La post-condition est vérifié juste avant de quitter la méthode. Le comportement au moment de l'exécution des post-conditions non réussies est déterminé par l'analyseur au moment de l'exécution.

Contrairement aux conditions préalables, les post-conditions peuvent référencer des membres avec moins de visibilité. Il est possible qu'un client ne soit pas en mesure de comprendre ou d'utiliser certaines des informations exprimées par une post-condition utilisant un état privé, mais cela n'affecte pas la capacité du client à utiliser la méthode correctement.

Post-conditions standard

Vous pouvez exprimer les post-conditions standard à l'aide de la méthode Ensures. Les post-conditions expriment une condition qui doit être true à l'arrêt normal de la méthode.

Contract.Ensures( this .F > 0 );

Post-conditions exceptionnelles

Les post-conditions exceptionnelles sont des post-conditions qui doivent être true lorsqu'une exception particulière est levée par une méthode. Vous pouvez spécifier ces post-conditions à l'aide de la méthode Contract.EnsuresOnThrow, comme le montre l'exemple suivant.

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

L'argument est la condition qui doit être true chaque fois qu'une exception qui est un sous-type de T est levée.

Certains types d'exception sont difficiles à utiliser dans une post-condition exceptionnelle. Par exemple, l'utilisation du type Exception pour T nécessite que la méthode garantisse la condition indépendamment du type d'exception levée, même s'il s'agit d'un dépassement de capacité de la pile ou d'une autre exception impossible à contrôler. Vous devez utiliser les post-conditions exceptionnelles uniquement pour des exceptions spécifiques qui peuvent être levées lorsqu'un membre est appelé, par exemple, lorsqu'une InvalidTimeZoneException est levée pour un appel de méthode TimeZoneInfo.

Post-conditions spéciales

Les méthodes suivantes peuvent être utilisées uniquement au sein de post-conditions :

Vus pouvez faire référence aux valeurs de retour de la méthode dans les post-conditions à l'aide de l'expression Contract. Result<T>(), où T est remplacé par le type de retour de la méthode. Lorsque le compilateur ne parvient pas à déduire le type, vous devez le fournir explicitement. Par exemple, le compilateur C# ne peut pas déduire des types pour les méthodes qui ne prennent pas d'arguments. Il nécessite donc la post-condition suivante : les Méthodes Contract.Ensures(0 < Contract.Result<int>()) Les méthodes possédant le type de retour void ne peuvent pas faire référence à Contract. Result<T>() dans leurs post-conditions.

Une valeur « prestate » dans une post-condition fait référence à la valeur d'une expression au démarrage d'une méthode ou propriété. Elle utilise l'expression Contract.OldValue<T>(e), où T est le type de e. Vous pouvez omettre l'argument de type générique chaque fois que le compilateur est en mesure de déduire son type. (Par exemple, le compilateur C# déduit toujours le type car il utilise un argument.) Il existe plusieurs restrictions sur ce qui peut se produire dans e et les contextes dans lesquels une expression ancienne peut s'afficher. Une expression ancienne ne peut pas contenir une autre expression ancienne. Encore plus important, une expression ancienne doit faire référence à une valeur qui a existé dans l'état de condition préalable de la méthode. En d'autres termes, il doit s'agir d'une expression qui peut être évaluée tant que la condition préalable de la méthode est true. Voici plusieurs instances de cette règle.

La valeur doit exister dans l'état de condition préalable de la méthode. Pour référencer un champ sur un objet, les conditions préalables doivent garantir que cet objet est toujours non null.
Vous ne pouvez pas faire référence à la valeur de retour de la méthode dans une expression ancienne :
```
Contract.OldValue(Contract.Result<int>() + x) // ERROR
```
Vous ne pouvez pas faire référence aux paramètres out dans une expression ancienne.
Une expression ancienne ne peut pas dépendre de la variable limitée d'un quantificateur si la plage du quantificateur dépend de la valeur de retour de la méthode :
```
Contract. ForAll (0,Contract. Result<int>(),
i => Contract.OldValue(xs[i]) > 3 ); // ERROR
```
Une expression ancienne ne peut pas faire référence au paramètre du délégué anonyme dans un appel ForAll ou Exists à moins qu'elle ne soit utilisée en tant qu'indexeur ou argument à un appel de méthode :
```
Contract. ForAll (0, xs .Length, i => Contract.OldValue(xs[i]) > 3); // OK
Contract. ForAll (0, xs .Length, i => Contract.OldValue(i) > 3 ); // ERROR
```
Une expression ancienne ne peut pas se produire dans le corps d'un délégué anonyme si la valeur de l'expression ancienne dépend de l'un des paramètres du délégué anonyme, à moins que le délégué anonyme ne soit un argument à la méthode ForAll ou Exists :
```
Method( ... (T t) => Contract.OldValue(... t ...) ... ); // ERROR
```

Les paramètres Out posent un problème car les contrats apparaissent avant le corps de la méthode, et la plupart des compilateurs n'autorisent pas de références aux paramètres out dans les post-conditions. Pour résoudre ce problème, la classe Contract fournit la méthode ValueAtReturn<T>, ce qui autorise une post-condition basée sur un paramètre out.

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

Comme avec la méthode OldValue<T>, vous pouvez omettre le paramètre de type générique chaque fois que le compilateur est en mesure de déduire son type. Le rewriter de contrat remplace l'appel de méthode par la valeur du paramètre out. La méthode ValueAtReturn<T> peut apparaître uniquement dans des post-conditions. L'argument à la méthode doit être un paramètre out ou un champ d'un paramètre out de structure. Ce dernier est également utile lors de la référence aux champs dans la post-condition d'un constructeur de structure.

Remarque
Actuellement, les outils d'analyse de contrat de code ne vérifient pas si les paramètres out sont correctement initialisés et ignorent leur mention dans la post-condition.Par conséquent, dans l'exemple précédent, si la ligne après le contrat avait utilisé la valeur de x au lieu de lui assigner un entier, un compilateur n'aurait pas émis l'erreur correcte.Toutefois, sur une génération où le symbole de préprocesseur CONTRACTS FULL n'est pas défini (tel qu'une version Release ), le compilateur émet une erreur.

Actuellement, les outils d'analyse de contrat de code ne vérifient pas si les paramètres out sont correctement initialisés et ignorent leur mention dans la post-condition.Par conséquent, dans l'exemple précédent, si la ligne après le contrat avait utilisé la valeur de x au lieu de lui assigner un entier, un compilateur n'aurait pas émis l'erreur correcte.Toutefois, sur une génération où le symbole de préprocesseur CONTRACTS FULL n'est pas défini (tel qu'une version Release ), le compilateur émet une erreur.

Invariants

Les invariants objet sont des conditions qui doivent être remplies pour chaque instance d'une classe chaque fois que cet objet est visible à un client. Ils expriment les conditions sous lesquelles l'objet est considéré comme étant correct.

Les méthodes invariantes sont identifiées par l'attribut ContractInvariantMethodAttribute. Elles ne doivent contenir aucun code à l'exception d'une séquence d'appels à la méthode Invariant, chacun spécifiant un invariant individuel, comme indiqué dans l'exemple suivant.

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

Les invariants sont définis de façon conditionnelle par le symbole de préprocesseur CONTRACTS FULL. Pendant le contrôle à l'exécution, les invariants sont vérifiés à la fin de chaque méthode publique. Si un invariant mentionne une méthode publique dans la même classe, le contrôle d'invariant qui se produirait normalement à la fin de cette méthode publique est désactivé. À la place, le contrôle se produit uniquement à la fin de l'appel de méthode le plus à l'extérieur de cette classe. Cela se produit également si la classe est à nouveau entrée à cause d'un appel à une méthode sur une autre classe. Les invariants ne sont pas vérifiés pour les finaliseurs d'objet ou pour les méthodes qui implémentent la méthode Dispose.

Indications relatives à l'utilisation

Classement de contrat

Le tableau suivant indique l'ordre des éléments que vous devez utiliser lorsque vous écrivez des contrats de méthode.

If-then-throw statements	Conditions préalables publiques à compatibilité descendante
Requires	Toutes les conditions préalables publiques.
Ensures	Toutes les post-conditions publiques (normales).
EnsuresOnThrow	Toutes les post-conditions exceptionnelles publiques.
Ensures	Toutes les post-conditions privées/internes (normales).
EnsuresOnThrow	Toutes les post-conditions exceptionnelles privées/internes.
EndContractBlock	Si vous utilisez des conditions préalables de style if-then-throw sans autres contrats, passez un appel à EndContractBlock pour indiquer que tous les contrôles if préalables sont des conditions préalables.

Pureté

Toutes les méthodes appelées dans un contrat doivent être pures ; autrement dit, elles ne doivent pas mettre à jour un état préexistant. Une méthode pure a l'autorisation de modifier des objets créés après l'entrée dans la méthode pure.

Les outils de contrat de code supposent actuellement que les éléments de code suivants sont purs :

Méthodes marquées avec l'attribut PureAttribute.
Types marqués avec l'attribut PureAttribute (l'attribut s'applique à toutes les méthodes du type).
Accesseurs get de propriété.
Opérateurs (méthodes statiques dont le nom commence par « op », et qui ont un ou deux paramètres et un type de retour non void).
Toute méthode dont le nom qualifié complet commence par « System.Diagnostics.Contracts.Contract », « System.String », « System.IO.Path » ou « System.Type ».
Tout délégué appelé, à condition que le type délégué lui-même soit attribué avec l'attribut PureAttribute. Les types délégués System.Predicate<T> et System.Comparison<T> sont considérés comme purs.

Visibilité

Tous les membres indiqués dans un contrat doivent être au moins aussi visibles que la méthode dans laquelle ils apparaissent. Par exemple, un champ privé ne peut pas être mentionné dans une condition préalable pour une méthode publique ; les clients ne peuvent pas valider un tel contrat avant d'appeler la méthode. Cependant, si le champ est marqué avec l'attribut ContractPublicPropertyNameAttribute, il est exempté de ces règles.

Exemple

L'exemple suivant illustre l'utilisation des contrats de code.

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