[.NET] Code Contracts – Partie 2 – Les pré-conditions

Ce post fait suite à une introduction sur Code Contracts. Il explique ce qu’est une pré-condition, comment les définir et aussi comment les activer à l’aide de l’outil de réécriture.

Ce post fait partie d’une série de post consacré à Code Contracts :

Qu’est ce qu’une pré-condition ?

Une pré-condition est un contrat que doit respecter un appelant pour utiliser une méthode où une propriété. Le plus souvent les pré-conditions permettent de contrôler les paramètres d’une méthode, mais on peut les utiliser pour définir des contrats sur l’état que doit avoir un objet lors de l’appel à une méthode.

Comment définir une pré-condition ?

Code Contracts permet de définir très simplement un contrat à l’aide de la méthode Contract.Requires() :

public static double Diviser(int dividende, int diviseur)
{
    Contract.Requires(diviseur != 0, "Le diviseur ne peut pas être égale à 0");

    return dividende / diviseur;
}

Le premier paramètre est une expression booléenne qui représente le contrat et qui doit toujours être vrai pour que le contrat soit respecté. Le deuxième paramètre est une chaine de caractères qui représente une message d’erreur à afficher si le contrat n’est pas respecté.

Il est possible de spécifier plusieurs contrats, dans ce cas il faudra les spécifier les uns à la suite des autres. Il est aussi tout à fait possible de spécifier plusieurs contrats portant sur le même paramètre :

public static void Afficher(string nom, int age)
{
    Contract.Requires(nom != null);
    Contract.Requires(nom.Length > 3);
    Contract.Requires(1 <= age && age <= 99);

    Console.WriteLine("{0} : {1}", nom, age);
}

La méthode Contract.Requires() doit-être vue comme des méta-données…

La méthode Contract.Requires() ne doit pas être vu comme une méthode qui exécute du code, mais comme des méta-données de la méthode Diviser() (exactement comme des attributs .NET).

En effet, si on exécute la méthode Diviser() avec un diviseur à 0, aucun mécanisme de sécurité sur le contrat n’est déclenché. Le code continue son exécution jusqu’à levée une exception au niveau de la division par 0.

image

Pourtant si l’on regarde le code généré on se rend très vite compte que l’appel à la méthode Contract.Requires() a disparu :

image

Pourquoi ? Tout simplement parce qu’elle dispose d’un attribut conditionnel spécifiant que la macro CONTRACTS_FULL doit-être défini au moment de la compilation.

image

Si on défini la macro CONTRACTS_FULL dans les propriétés de projet…

image

Et que l’on relance l’application, un message d’avertissement apparait :

image

Ce message indique qu’il est nécessaire d’utiliser un outil de réécriture lorsque l’on utilise les pré-conditions à l’aide de Contract.Requires(). ccrewriter est l’un des outils inclus de Code Contracts qui permet de transformer les appels de la méthode Contract.Requires() en levée d’exception .NET.

L’activation de l’outil de réécriture ccrewriter se fait depuis l’onglet Code Contracts dans les paramètres de projet. Il suffit d’activer l’option “Perform Runtime Contract Checking” à “Full”. (Nous verrons plus en détail un peu plus-tard les options disponibles dans les paramètres de projet).

image

Après recompilation, une exception de type ContractException est levée si le diviseur passé en paramètre est égal à 0 :

image

Déclenchez une exception d’un autre type

Il existe une surcharge de la méthode Contract.Requires() qui est générique et qui permet de déclencher une exception autre que ContractException. Le type de l’exception à déclencher doit-être spécifié en paramètre de type à la méthode Contract.Requires(). Dans notre cas, si on veut lever une exception de type ArgumentException en cas de non respect de notre contrat, il faut écrire :

public static double Diviser(int dividende, int diviseur)
{
    Contract.Requires&lt;ArgumentException&gt;(diviseur != 0, "Le diviseur ne peut pas être égal à 0");

    return dividende / diviseur;
}

Pour que ce code puisse être compilé et réécrit avec ccrewriter, il est nécessaire de définir l’option “Assembly Mode” à “Standard Contract Requires” dans les propriétés du projet.

image

Après compilation, on obtient à l’exécution, la levée d’une exception de type ArgumentException lors que le diviseur passé en paramètre est à 0 :

image

Contrôler les paramètres de type IEnumerable<T> (ForAll() et Exists())

La classe Contract contient deux méthodes ForAll() et Exists() permettant de contrôler des éléments se trouvant dans une séquence de type IEnumerable<T>.

  • La méthode ForAll() vérifie que tous les éléments d’une séquence respecte la condition spécifiée en paramètre.
  • La méthode Exists() vérifie qu’au moins un élément d’une séquence respecte la condition spécifiée en paramètre.

Ces méthodes peuvent être vues comme un moyen simple de faire une simple boucle foreach dans des contrats. Dans les deux cas, les conditions sont spécifiés à l’aide d’une lambda expression. L’exemple qui suit montre comment vérifier que les éléments d’une séquence de noms ne soient pas null, vide ou contenant des espaces. Remarquez qu’il ne faut pas oublier d’ajouter un contrat permettant de vérifier que l’énumération passé en paramètre n’est pas null.

public static void Afficher(IEnumerable&lt;string&gt; noms)
{
    Contract.Requires&lt;ArgumentException&gt;(noms != null);
    Contract.Requires&lt;ArgumentException&gt;(Contract.ForAll(noms, nom => string.IsNullOrWhiteSpace(nom)) == false);

    foreach (string nom in noms)
    {
        Console.WriteLine(nom);
    }
}

Si l’on passe en paramètre une séquence (par exemple un tableau) contenant une chaine nulle ou vide on obtiendra l’exception suivante :

image

Il existe une surcharge supplémentaires pour les méthodes ForAll() et Exists() qui permettent d’incrémenter une variable et de vérifier une condition à chaque itération. Ces surcharges peuvent être vues comme un moyen de réaliser une boucle for dans des contrats. L’exemple suivant montre comment contrôler que tous les nombres d’un tableau spécifié en paramètre sont des nombres paires :

public static void Afficher(int[] t)
{
    Contract.Requires&lt;ArgumentException&gt;(t != null);
    Contract.Requires&lt;ArgumentException&gt;(Contract.ForAll(0, t.Length, i => t[i] % 2 == 0));

    foreach (int nombre in t)
    {
        Console.WriteLine(nombre);
    }
}

Fini le blabla ! Laisser parler votre code !

Une des forces de Code Contracts est la possibilité d’inclure la condition des contrats dans les messages d’erreur. Plus précisément, c’est l’outil de réécriture ccrewriter qui prend la condition booléenne C# et en fait une chaine de caractères pour l’inclure dans les messages d’erreur.

image

Ainsi, il n’est plus nécessaire d’écrire, de traduire et de maintenir une chaine de caractères représentant le message d’erreur affiché lorsqu’un contrat n’est pas valide.

Ce mécanisme permet d’avoir un certain “typage fort” entre vos contrats et les messages d’erreurs associés. En effet, si vous renommez un paramètre vous serai obligé de modifier les conditions des contrats associés (sinon la compilation est impossible). Il n’est donc plus nécessaire de modifier des chaines de caractères.

L’exemple suivant montre le code de la méthode Diviser() en supprimant le message d’erreur associé au contrat qui porte sur le diviseur :

public static double Diviser(int dividende, int diviseur)
{
    Contract.Requires&lt;ArgumentException&gt;(diviseur != 0);

    return dividende / diviseur;
}

A l’exécution, lorsque le contrat est invalide, l’appelant obtiendra l’exception suivante :

image

Ce post était consacré aux pré-conditions, nous verrons dans le prochain les post-conditions.

Stay tuned !

Publié dans la catégorie .NET Framework.
Tags : , , . TrackBack URL.

Un commentaire

  1. fred dit :

    Bonjour Gilles,
    Merci pour cette deuxième partie, c’est intéressant.
    Pour moi les codes contrats sont tellement évidents que je me demandais si Microsoft n’aurait pas tout intérêts à dériver ses classes afin de ne pas diviser par zéro ou afficher une chaine nulle dans le Framework 4.5.

Leave a comment