Nous avons vu précédemment comment définir des pré-conditions à l’aide de Code Contracts. Nous allons voir maintenant comment définir des post-conditions à l’aide de Code Contracts.
Ce post fait partie d’une série de post consacré à Code Contracts :
- Partie 01 – Introduction
- Partie 02 – Les pré-conditions
- Partie 03 – Les post-conditions
- Partie 04 – Les invariants
- Partie 05 – Les contrats sur les interfaces
Qu’est-ce qu’une post-condition ?
Une post-condition permet de définir un contrat qui devra être respecté avant de sortir d’une méthode (ou d’un getter/setter d’une propriété). Les post-conditions doivent être vue comme un contrat ou une assurance qu’un développeur va exposer aux appelants d’une méthode.
Code Contracts permet de définir 4 types de post-conditions :
- Sur la valeur de retour d’une méthode
- Sur la valeur d’un paramètre de sortie d’une méthode (paramètre de type out)
- Sur la valeur précédente (initiale) d’une propriété ou d’un paramètre d’une méthode.
- Sur la valeur d’une propriété ou d’un paramètre après la levée d’une exception dans une méthode
Les post-condition ne servent pas d’assertion !
Lorsque je présente les post-conditions, les développeurs sont souvent tentés d’utiliser les post-conditions comme un outil permettant de contrôler le retour d’une méthode. Bien que c’est le but de l’outil de ré-écriture ccrewriter, ce n’est vraiment pas la philosophie des post-conditions de Code Contracts.
Une post-condition doit-être vue comme un message que l’on souhaite passer au développeur qui utilisera notre méthode (ou à l’appelant). Si on prend comme exemple l’affirmation suivante : “L’appel de la méthode M() retournera toujours une référence vers un objet (plus techniquement la référence retournée ne sera jamais nulle)”. Le développeur (ou l’intégrateur) qui utilisera la méthode M(), sera qu’il n’est pas nécessaire de tester la nullité de la référence récupérée par la méthode M().
Contrairement aux pré-conditions, si le contrat n’est pas validé, ce n’est pas la faute de l’appelant mais au concepteur de la méthode !
Comment définir une post-condition ?
Code Contracts permet de définir très simplement une post-condition à l’aide de la méthode Contract.Ensures(). Cette méthode doit-être spécifiée au début du corps de la méthode avec les pré-conditions.
Comme pour les pré-conditions, la méthode Contract.Ensures() prend en paramètre la condition à vérifier et si nécessaire un message explicatif associé.
L’exemple suivant, montre une post-condition qui garanti que la propriété MonObjet fera référence à un objet.
public class MonObjet
{
public string Message
{
get;
private set;
}
public void RemplirMessage()
{
Contract.Ensures(this.Message != null);
this.Message = "Hello !";
}
}
Comme pour les pré-conditions, il faut voir les appels à la méthode Contract.Ensures() comme des méta-données. Ce sont les outils lancées après la compilation qui permettront d’interpréter ce genre de contrats.
En utilisant l’exemple précédent, il est donc possible d’appeler la méthode RemplirMessage() et d’utiliser directement la propriété Message sans tester sa nullité.
MonObjet instance = new MonObjet(); instance.RemplirMessage(); char c = instance.Message[0];
Si maintenant on active l’outil de ré-écriture de Code Contracts (je vous invite à consulter mon post précédent pour plus d’informations) et que le contrat n’est pas valide (c’est à dire si la propriété Message est à null en sortie de la méthode) on obtiendra l’exception suivante :
Définir une post-condition sur la valeur de retour d’une méthode.
Code Contracts permet de définir des post-conditions sur la valeur de retour d’une méthode. Pour cela il faut utiliser la méthode Contract.Result<T>(), avec T le type de retour de la méthode.
La méthode Contract.Result<T>() est une méta-données qui représente la valeur de retour de la méthode courante. L’exemple suivant illustre une méthode GetClients() retournant un tableau de client qui ne doit pas être null :
public Client[] GetClients()
{
Contract.Ensures(Contract.Result<Client[]>() != null);
return new Client[]
{
new Client() { Nom = "TOURREAU" }
};
}
Ce genre de post-condition apporte une information importante pour l’appelant. En effet, le résultat de l’appel de la méthode GetClients() peut-être directement utilisé dans une boucle de type foreach car le tableau obtenu ne sera jamais null (une vérification de l’existence d’un tableau n’est donc pas nécessaire au niveau de l’appelant).
MonObjet instance = new MonObjet();
foreach (Client client in instance.GetClients())
{
Console.WriteLine(client.Nom);
}
Définir une post-condition sur un paramètre de sortie d’une méthode.
Code Contracts offre une méthode Contract.ValueAtReturn() permettant de définir des post-conditions sur des paramètres de sortie d’une méthode (paramètre de type out) :
public void GetMessage(out string message)
{
Contract.Ensures(Contract.ValueAtReturn(out message) != null);
message = "Hello !";
}
Dans cet exemple, la post-conditions définie permet d’assurer à l’appelant que le paramètre de sortie message sera toujours différent de null.
Définir une post-condition sur la valeur précédente d’un paramètre ou d’une propriété.
Code Contracts offre une fonctionnalité très puissante permettant de définir des post-conditions sur les valeurs initiales d’un paramètre ou d’une propriété. La méthode Contract.OldValue<T>() représente une méta-données qui correspond à la valeur initiale d’un paramètre ou d’une propriété.
L’outil de ré-écriture ccrewriter s’occupera d’insérer les variables temporaires permettant de comparer les valeurs des paramètres ou des propriétés au début et à la fin de l’appel à une méthode.
Imaginons une classe contenant un compteur (propriété) et une méthode qui affiche et incrémente ce compteur. Il serait intéressant dans la méthode d’exposer une post-condition qui indique que la valeur du compteur aie bien été incrémentée :
public class MonObjet
{
public int Compteur
{
get;
set;
}
public void Compter()
{
Contract.Ensures(Contract.OldValue(this.Compteur) + 1 == this.Compteur);
Console.WriteLine(this.Compteur);
this.Compteur++;
}
}
Définir une post-condition sur la valeur d’un paramètre ou d’une propriété après la levée d’une exception.
Code Contracts permet de définir une post-condition sur un paramètre ou une propriété après la levée d’une exception. Cela est très pratique pour indiquer à l’appelant que certaines propriétés ne sont pas modifiées ou sont réinitialisée en cas de levée d’une exception.
Pour définir ce genre de post-condition il faut utiliser la méthode Contract.EnsuresOnThrow<T>() avec T le type d’exception qui doit être déclenché pour vérifier la condition.
public class MonObjet
{
public string Message
{
get;
set;
}
public void UpdateMessage(bool déclencherException)
{
Contract.EnsuresOnThrow<InvalidOperationException>(this.Message == null);
if (déclencherException == true)
{
this.Message = null;
throw new InvalidOperationException();
}
this.Message = "Hello !";
}
}
Dans l’exemple précédent, l’appelant peut avoir l’assurance que la propriété Message sera à null si la méthode UpdateMessage() déclenche une exception de type InvalidOperationException.
Ce post était consacré aux post-conditions, nous verrons dans le prochain les invariants.
Stay tuned !