Envie de savoir si votre code fonctionne avant même de l’exécuter, vous en rêvez, Microsoft l’a fait !

Présentation de l’outil

Code Contracts permet de définir des contrats. Un contrat peut prendre la forme d’une précondition (état au début d’une méthode), d’une post-condition (état à la fin d’une méthode) ou d’un invariant (état vrai tout le temps). Ces contrats peuvent être vérifiés à l’exécution ou à la compilation.

Les objectifs de Code Contracts sont :

  • D’ajouter des informations complémentaires sur le comportement du code. Cela permet notamment de comprendre pourquoi les choses ne se passent pas comme prévus (mauvais arguments, valeur de retour exigüe, effet de bord non désiré, etc. )
  • De vérifier statiquement le code
  • D’améliorer la documentation en y intégrant les contrats.

Installation

Afin d’utiliser Code Contracts, il vous suffit de télécharger les binaires d’installation. Ceux-ci sont disponibles sur le site de Microsoft à l’adresse suivante : http://research.microsoft.com/en-us/projects/contracts/.   A noter que l’outil est compatible avec Visual Studio 2010, 2012 et 2013 et qu’un package nugget non officiel est également à votre disposition : https://www.nuget.org/packages/CodeContracts.Unofficial/.

Pour l’installation, rien de plus simple : suivant, suivant, suivant et un dernier clic sur terminer.

Comment ça fonctionne

Code Contracts est composé de 3 outils :

  • ccrewrite : Modifie l’exécutable ou la DLL après la compilation pour générer les vérifications lors de l’exécution

Avant ccrewrite :

public static int Fact(int n) 
{ 
   Contract.Requires(n >= 0); // Précondition 
   Contract.Ensures(Contract.Result<int>() > 0); // Postcondition 
   return n == 0 ? 1 : n * Fact(n - 1); // Code 
}

Après ccrewrite :

public static int Fact(int n) 
{ 
   __ContractsRuntime.Requires(n >= 0, (string) null, "n >= 0");// Précondition 
   int num = n == 0 ? 1 : n * Program.Fact(n - 1); // Code 
   __ContractsRuntime.Ensures(num > 0, (string) null, "Contract.Result<int>() > 0");// Postcondition 
   return num; 
}
  • cccheck : effectue la vérification statique des contrats (i. e. au moment de la compilation)

Code Contracts détecte que la précondition n’est pas respectée (ça fonctionne aussi avec des cas plus complexes :)).

  • ccdoc : Ajoute les contrats dans la documentation XML ce qui permet d’avoir une documentation à jour (au moins pour les contrats).
<?xml version="1.0"?> 
<doc> 
  <assembly> 
   <name>DemoCodeContracts</name> 
  </assembly> 
  <members> 
   <member name="M:DemoCodeContracts.Program.Fact(System.Int32)"> 
   <requires csharp="n &gt;= 0" vb="n &gt;= 0">n &gt;= 0</requires>
   <ensures csharp="result &gt; 0" vb="result &gt; 0">result &gt; 0</ensures> 
   </member> 
  </members> 
</doc>

Les différents types de contrats

Les préconditions

Les préconditions permettent de vérifier l’état au début de la méthode. Le classique if-then-throw se transforme en Contract. Requires<ExceptionType> (condition)ExceptionType est facultatif et permet de choisir le type de l’exception lancé lorsque le contrat n’est pas respecté. Il est présent pour permettre à vos anciens codes d’évoluer ou bien de lancer une exception précise pour une API.

Contract.Requires(str != null); 
Contract.Requires<ArgumentNullException>(str != null);

Les post-conditions

Les post-conditions permettent de vérifier l’état à la fin de la méthode. Par exemple on va donc pouvoir s’assurer que la valeur de retour n’est pas null :

Contract.Ensures(Contract.Result<string>() != null);

Contract. Result<T> () permet de designer le valeur de retour de la méthode. Le paramètre T est le type de retour de la fonction. On peut aussi définir des post-conditions sur les argument de type out grâce à Contract. ValueAtReturn (out result). On peut ainsi écrire

Contract.Ensures(Contract.ValueAtReturn(out result) == "foobar");

Les invariants

Un invariant est une condition toujours respectée. Par exemple, dans le cas d’une Fraction, le dénominateur est toujours différent de 0. Ces invariants ne sont pas spécifiques à une méthode, mais à une classe. Comme on ne peut pas déclarer les contrats directement dans la classe, la solution est de créer une méthode décorée par l’attribut ContractInvariantMethod. Les invariants seront testés à la fin de chaque appel d’une méthode publique de l’objet.

[ContractInvariantMethod] 
void Invariants() 
{ 
   Contract.Invariant(this.Denominator > 0); 
}

Les interfaces et les classes abstraites

Il est théoriquement impossible de définir des contraintes sur les interfaces ou les méthodes abstraites d’une classe du fait qu’elles n’ont pas d’implémentation. Avec Code Contracts cela devient possible. Pour cela il faut créer une classe implémentant l’interface ou la classe abstraite et y définir les contrats. Ensuite on indique à Code Contracts que cette classe contient les contrats de l’interface à l’aide de l’attribut ContractClass (typeof (Implementation)) et en décorant la classe implémentant l’interface ou l’interface avec l’attribut ContractClassFor (typeof (Interface)).

ContractClass(typeof(RandomGeneratorContracts)) 
public interface IRandomGenerator 
{ 
   int Next(int min, int max); 
} 
  
ContractClassFor(typeof(IRandomGenerator)) 
sealed class RandomGeneratorContracts : IRandomGenerator 
{ 
   public int Next(int min, int max) 
   { 
   Contract.Requires<ArgumentOutOfRangeException>(min < max, 
"Min must be less than max"); 
   Contract.Ensures(Contract.Result<int>() >= min && Contract.Result<int>() <= max, 
"Return value is out of range"); 
   return default(int); 
   } 
}

L’interface de configuration de Code Contracts

La configuration de Code Contracts se fait directement depuis Visual Studio. Les options permettent de configurer le comportement des 3 outils de Code Contracts (ccrewriter, cccheck, ccdoc). On peut ainsi indiquer si les contrats doivent être réécrits et pour quelle partie du code. Au niveau de la vérification statique de nombreuses options sont disponibles. Leur utilisation influence le temps de vérification et la précision des résultats.

configuration

Conclusion

Code Contracts est simple à utiliser. Pour la réécriture du code et la documentation, rien à signaler. Cependant la vérification statique est plus hasardeuse. Certains cas semblent triviaux mais ne sont pas correctement compris par Code Contracts qui génèrent donc des faux positifs. De plus à partir de quelques milliers de lignes de code, le temps d’exécution du vérifieur statique devient très long (plusieurs minutes) et nécessite pas mal de RAM (supérieur à 1GO). La vérification statique est donc difficile à exécuter sur son poste, cependant il est possible de l’intégrer au processus de Build sur un serveur.

Voilà pour l’essentiel des fonctionnalités, n’hésitez pas à lire la documentation avant de commencer à utiliser Code Contracts : http://research.microsoft.com/en-us/projects/contracts/