Contrats de code (.NET Framework)

  • Article

Les contrats de code offrent un moyen de spécifier des préconditions, des postconditions et des invariants d’objet dans du code .NET Framework. Les conditions préalables sont des exigences qui doivent être satisfaites à l'entrée d'une méthode ou d'une propriété. Les post-conditions décrivent les attentes à la sortie de la méthode ou de la propriété. Les invariants d'objet décrivent l'état attendu pour une classe présentant un état correct.

Notes

Les contrats de code ne sont pas pris en charge dans .NET 5+ (y compris les versions de .NET Core). Envisagez d’utiliser à la place des types de référence Nullables.

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 contrats de code offrent les avantages suivants :

  • Tests améliorés : les contrats de code permettent la vérification de contrat statique, la vérification au moment de l'exécution et la génération de documentation.

  • Outils de test automatique : 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 remplissent 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érencements et des limites de tableau null, ainsi que des contrats explicites.

  • Documentation de référence : le générateur de documentation complète les fichiers de documentation XML existants avec des informations de contrat. Des feuilles de style peuvent également être utilisées avec Sandcastle pour ajouter des sections de contrat dans les pages de documentation générées.

Tous les langages .NET Framework peuvent directement utiliser les contrats, sans que vous ayez besoin de développer un analyseur ou compilateur spécial. Un complément Visual Studio vous permet de spécifier le niveau d'analyse de contrats de code à effectuer. Les analyseurs peuvent vérifier que les contrats sont correctement écrits (contrôle de type et résolution de noms), et créer 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 fonctionnalité IntelliSense standard fournie par l'outil.

La plupart des méthodes dans la classe de contrat sont compilées de façon conditionnelle : le compilateur émet des appels à ces méthodes seulement si vous définissez le symbole spécial CONTRACTS_FULL en utilisant la directive #define. Avec CONTRACTS_FULL, vous pouvez écrire des contrats dans votre code sans utiliser de directives #ifdef, et générer ainsi différentes builds, avec et sans contrats.

Pour obtenir des outils et des instructions détaillées sur l’utilisation des contrats de code, consultez Contrats de code sur le site Visual Studio Marketplace.

Preconditions

Vous pouvez spécifier des conditions préalables à l'aide de la méthode Contract.Requires. Les conditions préalables définissent l'état à l'appel d'une méthode. Elles sont généralement utilisées pour indiquer des valeurs de paramètre valides. Tous les membres spécifiés dans les conditions préalables doivent être au moins aussi accessibles que la méthode elle-même. Autrement, la condition préalable risque de ne pas être comprise par tous les appelants de la 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 spécifie que le paramètre x ne doit pas être null.

Contract.Requires(x != null);

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

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

Instructions Requires héritées

Dans la plupart des cas, le code contient du code de validation de paramètres sous la forme d’instructions if-then-throw. Les outils de contrat reconnaissent ces instructions comme étant des conditions préalables dans les cas suivants :

Quand 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 précondition réelle serait x != null.) Une précondition négative est très restreinte. Elle doit être écrite comme indiqué dans l’exemple précédent : elle ne doit pas contenir de clauses else et le corps de la clause then doit être une seule instruction throw. Le test if est soumis aux règles de pureté et à celles de visibilité (voir Indications relatives à l’utilisation), mais l’expression throw est soumise uniquement 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 relatifs à l'état d'une méthode qui se termine. La post-condition est vérifiée juste avant la sortie de 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 ayant moins de visibilité. Il est possible qu'un client ne puisse pas comprendre ou utiliser certaines des informations spécifiées par une post-condition avec un état privé, mais cela n'empêche pas le client d'utiliser la méthode correctement.

Post-conditions standard

Vous pouvez spécifier 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 quand une exception particulière est levée par une méthode. Vous pouvez les spécifier à 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. Utilisez les post-conditions exceptionnelles uniquement pour des exceptions spécifiques qui peuvent être levées après l'appel d'un membre, par exemple, quand une exception 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 :

  • Vous 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. Si le compilateur ne peut pas déduire le type, vous devez le fournir explicitement. Par exemple, le compilateur C# ne peut pas déduire les types des méthodes qui ne prennent pas d'arguments. Il nécessite donc la post-condition suivante : 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 de « pré-état » dans une post-condition fait référence à la valeur d'une expression au début d'une méthode ou d'une 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# infère toujours le type, car il prend un argument.) Il existe plusieurs restrictions sur ce qui peut se produire dans e et les contextes dans lesquels une ancienne expression peut apparaître. 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 préconditions doivent garantir que l’objet a toujours une valeur 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 lié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, sauf si elle est utilisée en tant qu’indexeur ou argument pour 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 s'utiliser 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 de la méthode ForAll ou Exists :

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

    • Les paramètres Out posent un problème, car les contrats sont placés avant le corps de la méthode, et la plupart des compilateurs n'autorisent pas les 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, qui permet d'utiliser une post-condition basée sur un paramètre out.

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

      Comme avec la méthode OldValue, 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 module de réécriture de contrat remplace l'appel de méthode par la valeur du paramètre out. La méthode ValueAtReturn peut apparaître uniquement dans des post-conditions. L’argument de la méthode doit être un paramètre out ou un champ d’un paramètre out de structure. Ce dernier est également utile pour faire référence aux champs dans la post-condition d'un constructeur de structure.

      Notes

      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. Si, dans l'exemple précédent, la ligne après le contrat avait utilisé la valeur de x au lieu de lui assigner un nombre entier, un compilateur n'aurait donc pas généré l'erreur correspondante. Toutefois, dans une build où le symbole de préprocesseur CONTRACTS_FULL n’est pas défini (telle qu’une build de mise en production), le compilateur génère une erreur.

Invariants

Les invariants d'objet sont des conditions qui doivent être remplies (true) pour chaque instance d'une classe dès que cet objet est visible par un client. Ils spécifient 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. Ils sont vérifiés au moment de l'exécution à la fin de chaque méthode publique. Si un invariant spécifie une méthode publique dans la même classe, la vérification d'invariant prévue normalement à la fin de cette méthode publique est désactivée. À la place, la vérification 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 un finaliseur d’objet et une implémentation de IDisposable.Dispose.

Instructions d’utilisation

Classement de contrat

Le tableau suivant indique l'ordre des éléments à utiliser quand 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 standard publiques
EnsuresOnThrow Toutes les post-conditions exceptionnelles publiques
Ensures Toutes les post-conditions standard privées/internes
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, ajoutez un appel à EndContractBlock pour indiquer que toutes les vérifications if précédentes sont des conditions préalables.

Pureté

Toutes les méthodes appelées dans un contrat doivent être pures, c'est-à-dire qu'elles ne doivent pas mettre à jour un état préexistant. Une méthode pure peut modifier des objets qui ont été créés après l'entrée dans la méthode pure.

Les outils de contrat de code considèrent 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 (cet 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 », qui comportent un ou deux paramètres et dont le type de retour n’est pas void).

  • Méthodes dont le nom qualifié complet commence par « System.Diagnostics.Contracts.Contract », « System.String », « System.IO.Path » ou « System.Type ».

  • Les délégués appelés, à 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 spécifié dans une condition préalable pour une méthode publique, car 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.

#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