Partager via

Contrats de code (.NET Framework)

Remarque

Cet article est spécifique à .NET Framework. Elle ne s’applique pas aux implémentations plus récentes de .NET, notamment .NET 6 et versions ultérieures.

Les contrats de code permettent de spécifier les conditions préalables, les postconditions et les invariants d’objets dans le code .NET Framework. Les conditions préalables sont des exigences qui doivent être remplies lors de 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’objets décrivent l’état attendu d’une classe qui est dans un bon état.

Remarque

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

Les contrats de code incluent des classes pour marquer votre code, un analyseur statique pour l’analyse au moment de la compilation et un analyseur d’exécution. Les classes pour les contrats de code se trouvent dans l'espace de nom System.Diagnostics.Contracts.

Les avantages des contrats de code sont les suivants :

  • Amélioration des tests : les contrats de code fournissent la vérification statique des contrats, la vérification du runtime et la génération de documentation.

  • Outils de test automatiques : vous pouvez utiliser des contrats de code pour générer des tests unitaires plus significatifs en filtrant les arguments de test sans signification qui ne répondent pas aux conditions préalables.

  • Vérification statique : le vérificateur statique peut décider s’il existe des violations de contrat sans exécuter le programme. Il vérifie les contrats implicites, tels que les inférences null et les limites de tableau, et les 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 existe également des feuilles de style qui peuvent être utilisées avec Sandcastle afin que les pages de documentation générées aient des sections de contrat.

Tous les langages .NET Framework peuvent immédiatement tirer parti des contrats ; vous n’avez pas besoin d’écrire un analyseur ou un compilateur spécial. Un complément Visual Studio vous permet de spécifier le niveau d’analyse du contrat de code à effectuer. Les analyseurs peuvent confirmer que les contrats sont bien formés (vérification de type et résolution de noms) et peuvent produire une forme compilée des contrats au format CIL (Common Intermediate Language). La création de contrats dans Visual Studio vous permet de tirer parti de la norme IntelliSense fournie par l’outil.

La plupart des méthodes de la classe de contrat sont compilées de manière conditionnelle ; autrement dit, le compilateur émet des appels à ces méthodes uniquement lorsque vous définissez un symbole spécial, CONTRACTS_FULL, à l’aide de la #define directive. CONTRACTS_FULL vous permet d’écrire des contrats dans votre code sans utiliser #ifdef de directives ; vous pouvez produire différentes builds, certaines avec des contrats et certaines sans.

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

Conditions préalables

Vous pouvez exprimer des conditions préalables à l’aide de la Contract.Requires méthode. Les conditions préalables spécifient l’état lorsqu’une méthode est appelée. Ils sont généralement utilisés pour spécifier 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 ; sinon, 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 d’exécution des conditions préalables ayant échoué est déterminé par l’analyseur d’exécution.

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

Contract.Requires(x != null);

Si votre code doit lever une exception particulière en cas de défaillance d’une condition préalable, vous pouvez utiliser la surcharge générique de Requires de la manière suivante.

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

Instructions Requires héritées

La plupart du code contient une validation de paramètre sous la forme de if-then-throw code. Les outils de contrat reconnaissent ces instructions comme des conditions préalables dans les cas suivants :

  • Les instructions apparaissent avant toute autre instruction d’une méthode.

  • L’ensemble entier de ces instructions est suivi d’un appel de méthode explicite, tel qu’un appel à la méthode Contract, Requires, Ensures, ou EnsuresOnThrow.

Lorsque if-then-throw les instructions apparaissent sous ce formulaire, les outils les reconnaissent comme des instructions héritées.requires Si aucun autre contrat ne suit la if-then-throw séquence, terminez le code par la Contract.EndContractBlock méthode.

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

Notez que la condition dans le 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 fortement restreinte : elle doit être écrite comme indiqué dans l’exemple précédent ; c’est-à-dire, elle ne doit contenir aucune clause else, et le corps de la clause then doit être une instruction unique throw. Le if test est soumis à des règles de pureté et de visibilité (voir Recommandations d’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 d’exécution des postconditions ayant échoué est déterminé par l’analyseur runtime.

Contrairement aux conditions préalables, les postconditions peuvent référencer des membres avec moins de visibilité. Un client peut ne pas être en mesure de comprendre ou d’utiliser certaines des informations exprimées par une postcondition à l’aide d’un état privé, mais cela n’affecte pas la capacité du client à utiliser correctement la méthode.

Post-conditions standard

Vous pouvez exprimer des postconditions standard à l’aide de la Ensures méthode. Les postconditions expriment une condition qui doit être true à l’arrêt normal de la méthode.

Contract.Ensures(this.F > 0);

Post-conditions exceptionnelles

Les postconditions exceptionnelles sont des postconditions qui doivent être true lorsqu’une exception particulière est levée par une méthode. Vous pouvez spécifier ces postconditions à l’aide de la Contract.EnsuresOnThrow méthode, comme l’illustre 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 exige que la méthode garantisse la condition peu importe le type d’exception levée, même s’il s’agit d’un dépassement de pile ou d’une autre exception impossible à contrôler. Vous devez utiliser des postconditions exceptionnelles uniquement pour des exceptions spécifiques qui peuvent être levées lors de l'appel d'un membre, par exemple lorsqu'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 méthode dans les postconditions à l’aide de l’expression Contract.Result<T>(), où T est remplacée 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 postcondition suivante : Contract.Ensures(0 <Contract.Result<int>()) Les méthodes avec un type de retour ne void peuvent pas faire référence Contract.Result<T>() dans leurs postconditions.

  • Une valeur de préétat dans une postcondition fait référence à la valeur d’une expression au début d’une méthode ou d’une propriété. Il 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 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 ancienne expression ne peut pas contenir une autre ancienne expression. Plus important encore, une ancienne expression doit faire référence à une valeur qui existait 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 l’objet est toujours non null.

    • Vous ne pouvez pas faire référence à la valeur de retour de la méthode dans une ancienne expression :

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

    • Vous ne pouvez pas faire référence aux paramètres out dans une ancienne expression.

    • Une ancienne expression 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 comme indexeur ou argument dans 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 précédente ne peut pas être utilisée dans le corps d’un délégué anonyme si la valeur de l’expression précédente dépend de l’un des paramètres du délégué anonyme, sauf si le délégué anonyme est un argument pour la méthode ForAll ou Exists.

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

    • Out les paramètres présentent un problème, car les contrats apparaissent avant le corps de la méthode, et la plupart des compilateurs n’autorisent pas les références aux out paramètres dans les postconditions. Pour résoudre ce problème, la Contract classe fournit la ValueAtReturn méthode, qui permet une postcondition basée sur un out paramètre.

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

      Comme avec la OldValue méthode, vous pouvez omettre le paramètre de type générique chaque fois que le compilateur est en mesure de déduire son type. La réécriture de contrat remplace l’appel de la 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 out paramètre ou un champ d’un paramètre de structure out . Ce dernier est également utile pour faire référence aux champs dans la post-condition d'un constructeur de structure.

      Remarque

      Actuellement, les outils d’analyse du contrat de code ne vérifient pas si out les paramètres sont initialisés correctement et ignorent leur mention dans le postcondition. 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 affecter un entier, un compilateur n’émettrait pas l’erreur correcte. Toutefois, sur une build où le symbole de préprocesseur CONTRACTS_FULL n’est pas défini (par exemple, build de mise en production), le compilateur émet une erreur.

Invariants

Les invariants d’objets sont des conditions qui doivent être vraies pour chaque instance d’une classe chaque fois que cet objet est visible par un client. Ils expriment les conditions dans lesquelles l’objet est considéré comme correct.

Les méthodes invariantes sont identifiées en étant marquées avec l’attribut ContractInvariantMethodAttribute . Les méthodes invariantes ne doivent contenir aucun code, à l’exception d’une séquence d’appels à la Invariant méthode, chacune spécifiant une invariante individuelle, comme illustré 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 manière conditionnelle par le symbole de préprocesseur CONTRACTS_FULL. Pendant la vérification du runtime, les invariants sont vérifiés à la fin de chaque méthode publique. Si une méthode invariante mentionne une méthode publique dans la même classe, la vérification invariante qui se produit normalement à la fin de cette méthode publique est désactivée. Au lieu de cela, la vérification se produit uniquement à la fin de l’appel de méthode le plus externe à cette classe. Cela se produit également si la classe est de nouveau entrée à cause d'un appel de méthode sur une autre classe. Les invariants ne sont pas vérifiés pour un finaliseur d’objet et une IDisposable.Dispose implémentation.

Instructions d’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 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 ; autrement dit, ils ne doivent pas mettre à jour un état préexistant. Une méthode pure est autorisée à modifier les objets qui ont été 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 le PureAttribute.

  • Types marqués avec le PureAttribute (l’attribut s’applique à toutes les méthodes du type).

  • Accesseurs get de propriété.

  • Opérateurs (méthodes statiques dont les noms commencent par « op » et qui ont un ou deux paramètres et un type de retour non void).

  • Toute méthode dont le nom 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 le PureAttribute. Les types System.Predicate<T> délégués et System.Comparison<T> sont considérés comme purs.

Visibilité

Tous les membres mentionné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. Toutefois, si le champ est marqué avec le ContractPublicPropertyNameAttribute, il est exempté de ces règles.

Exemple :

L’exemple suivant montre l’utilisation de 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
  • Last updated on