Nous avons vu précédemment comment définir des post-conditions à l’aide de Code Contracts. Nous allons voir maintenant comment définir des invariants à 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’un invariant ?

Un invariant est contrat qui doit toujours être vérifié durant la vie d’un objet. On utilise le plus souvent les invariants pour valider constamment la validité d’une propriété publique d’une classe.

Comme pour les post-conditions, les invariants permettent de “rassurer” un intégrateur qu’une condition sur une propriété sera toujours vérifiée après chaque appel à une méthode ou getter/setter d’une propriété “publique” de la classe (publique pour l’intégrateur, cela peut donc être les méthodes et propriétés public ou protected).

Comment définir un invariant ?

Pour définir un invariant, il faut créer une méthode privée marquée de l’attribut ContractInvariantMethodAttribute qui contiendra les différents contrats (invariants). Pour spécifier un invariant, il faut utiliser la méthode Contract.Invariant() et spécifier une condition qui devra toujours être vérifiée.

L’exemple suivant illustre la définition d’un invariant sur la classe CompteBancaire afin que le Solde soit toujours supérieur à 0.

public class CompteBancaire
{
    public decimal Solde
    {
        get;
        private set;
    }

    public void Créditer(decimal montant)
    {
        this.Solde += montant;
    }

    public void Débiter(decimal montant)
    {
        this.Solde -= montant;
    }

    [ContractInvariantMethod]
    private void MonInvariant()
    {
        Contract.Invariant(this.Solde > 0);
    }
}

Une fois compilée, la méthode MonInvariant() fait partie de la classe comme toute méthode privée classique. L’outil de réécriture modifiera automatiquement le code afin que la méthode soit appelée après chaque méthodes ou getter/setter publiques.

Si maintenant on exécute l’exemple suivant :

static void Main(string[] args)
{
    CompteBancaire cb = new CompteBancaire();
    cb.Créditer(100);
    cb.Débiter(200);
}

Comme pour les post-conditions une exception de type ContractException est automatiquement levée :

Les invariants ne valident pas les champs/propriétés privées !

Beaucoup d’exemples sur d’autres site web montrent des invariants qui valident les champs et les propriétés privées. Même si cela est techniquement possible, c’est complètement aberrant d’un point de vue conceptuel. En effet, les invariants sont des contrats qui seront visibles par les intégrateurs. Les conditions doivent donc définir des constantes sur des objets publiques !

Par exemple, si un intégrateur ne respecte pas un invariant qui fait référence à un champ privé, il peut obtenir un message d’erreur comme ceci :

Comment peut-il savoir que la variable “s” correspond au solde du compte bancaire ???

Les conditions des invariants doivent donc porter sur des propriétés visibles par les intégrateurs (public ou protected).

Ce post était consacré aux invariants, nous verrons dans le prochain comment définir des contrats sur les interfaces.

Stay tuned !