Conception par contrat

La conception par contrat ( DbC ), également connue sous le nom de programmation par contrat , programmation par contrat et programmation par contrat , est une approche de conception de logiciels .

Elle prescrit aux concepteurs de logiciels de définir des spécifications d'interface formelles , précises et vérifiables pour les composants logiciels , qui étendent la définition ordinaire des types de données abstraits avec des préconditions , des postconditions et des invariants . Ces spécifications sont appelées « contrats », conformément à une métaphore conceptuelle des conditions et obligations des contrats commerciaux.

L’approche DbC suppose que tous les composants clients qui appellent une opération sur un composant serveur répondront aux conditions préalables spécifiées comme requises pour cette opération.

Lorsque cette hypothèse est considérée comme trop risquée (comme dans le cas d'un calcul multicanal ou distribué ), l' approche inverse est adoptée, ce qui signifie que le composant serveur teste que toutes les conditions préalables pertinentes sont remplies (avant ou pendant le traitement de la demande du composant client ) et répond avec un message d'erreur approprié dans le cas contraire.

Le terme a été inventé par Bertrand Meyer en relation avec sa conception du langage de programmation Eiffel et décrit pour la première fois dans divers articles à partir de 1986 et dans les deux éditions successives (1988, 1997) de son livre Object-Oriented Software Construction . Eiffel Software a déposé une demande d'enregistrement de marque pour Design by Contract en décembre 2003, et elle a été accordée en décembre 2004. Le propriétaire actuel de cette marque est Eiffel Software.

La conception par contrat trouve ses racines dans les travaux sur la vérification formelle , la spécification formelle et la logique de Hoare . Les contributions originales comprennent :

• Une métaphore claire pour guider le processus de conception
• L'application à l'héritage , en particulier un formalisme de redéfinition et de liaison dynamique
• L'application à la gestion des exceptions
• Le lien avec la documentation automatique des logiciels

L'idée centrale de DbC est une métaphore de la façon dont les éléments d'un système logiciel collaborent entre eux sur la base d' obligations et d'avantages mutuels . La métaphore est issue de la vie professionnelle, où un « client » et un « fournisseur » conviennent d'un « contrat » qui définit, par exemple, que :

• Le fournisseur doit fournir un certain produit (obligation) et est en droit d'attendre du client qu'il lui ait payé ses honoraires (prestation).
• Le client doit payer les frais (obligation) et a le droit d'obtenir le produit (prestation).
• Les deux parties doivent satisfaire à certaines obligations, telles que les lois et règlements, applicables à tous les contrats.

De même, si la méthode d’une classe en programmation orientée objet fournit une certaine fonctionnalité, elle peut :

• Attendez-vous à ce qu'une certaine condition soit garantie à l'entrée par tout module client qui l'appelle : la précondition de la méthode — une obligation pour le client et un avantage pour le fournisseur (la méthode elle-même), car elle le libère de la nécessité de gérer des cas en dehors de la précondition.
• Garantir une certaine propriété à la sortie : la postcondition de la méthode — une obligation pour le fournisseur, et évidemment un avantage (le principal avantage de l'appel de la méthode) pour le client.
• Maintenir une certaine propriété, supposée à l'entrée et garantie à la sortie : l' invariant de classe .

Le contrat est sémantiquement équivalent à un triplet de Hoare qui formalise les obligations. Cela peut être résumé par les « trois questions » auxquelles le concepteur doit répondre à plusieurs reprises dans le contrat :

• Que prévoit le contrat ?
• Que garantit le contrat ?
• Que prévoit le contrat ?

De nombreux langages de programmation disposent de fonctionnalités permettant de créer des assertions de ce type. Cependant, DbC considère que ces contrats sont si essentiels à l'exactitude du logiciel qu'ils devraient faire partie du processus de conception. En effet, DbC préconise d'écrire les assertions en premier . Les contrats peuvent être écrits par des commentaires de code , appliqués par une suite de tests , ou les deux, même s'il n'existe pas de support linguistique spécial pour les contrats.

La notion de contrat s'étend jusqu'au niveau de la méthode/procédure ; le contrat pour chaque méthode contiendra normalement les informations suivantes :

• Valeurs ou types d'entrée acceptables et inacceptables, et leurs significations
• Valeurs de retour ou types et leurs significations
• Valeurs ou types de conditions d'erreur et d'exception pouvant survenir, et leurs significations
• Effets secondaires
• Conditions préalables
• Postconditions
• Invariants
• (plus rarement) Garanties de performance, par exemple pour le temps ou l'espace utilisé

Les sous-classes d'une hiérarchie d'héritage sont autorisées à affaiblir les préconditions (mais pas à les renforcer) et à renforcer les postconditions et les invariants (mais pas à les affaiblir). Ces règles se rapprochent du sous-typage comportemental .

Toutes les relations de classe existent entre les classes client et les classes fournisseur. Une classe client est obligée d'effectuer des appels aux fonctions fournisseur lorsque l'état résultant du fournisseur n'est pas violé par l'appel client. Par la suite, le fournisseur est obligé de fournir un état de retour et des données qui ne violent pas les exigences d'état du client.

Par exemple, un tampon de données fournisseur peut exiger que des données soient présentes dans le tampon lorsqu'une fonction de suppression est appelée. Par la suite, le fournisseur garantit au client que lorsqu'une fonction de suppression termine son travail, l'élément de données sera effectivement supprimé du tampon. D'autres contrats de conception sont des concepts d' invariant de classe . L'invariant de classe garantit (pour la classe locale) que l'état de la classe sera maintenu dans les tolérances spécifiées à la fin de chaque exécution de fonction.

Lors de l'utilisation de contrats, un fournisseur ne doit pas essayer de vérifier que les conditions du contrat sont satisfaites - une pratique connue sous le nom de programmation offensive - l'idée générale étant que le code doit « échouer de manière flagrante », la vérification du contrat étant le filet de sécurité.

La propriété « fail hard » de DbC simplifie le débogage du comportement du contrat, car le comportement prévu de chaque méthode est clairement spécifié.

Cette approche diffère considérablement de celle de la programmation défensive , où le fournisseur est responsable de déterminer ce qu'il doit faire lorsqu'une condition préalable est rompue. Le plus souvent, le fournisseur génère une exception pour informer le client que la condition préalable a été rompue, et dans les deux cas (DbC comme programmation défensive), le client doit déterminer comment y répondre. Dans de tels cas, DbC facilite le travail du fournisseur.

La conception par contrat définit également des critères d’exactitude pour un module logiciel :

• Si l'invariant de classe ET la précondition sont vrais avant qu'un fournisseur ne soit appelé par un client, alors l'invariant ET la postcondition seront vrais une fois le service terminé.
• Lors des appels à un fournisseur, un module logiciel ne doit pas violer les conditions préalables du fournisseur.

La conception par contrat peut également faciliter la réutilisation du code, puisque le contrat pour chaque élément de code est entièrement documenté. Les contrats pour un module peuvent être considérés comme une forme de documentation logicielle pour le comportement de ce module.

Les conditions contractuelles ne doivent jamais être violées lors de l'exécution d'un programme sans bug. Les contrats ne sont donc généralement vérifiés qu'en mode débogage lors du développement du logiciel. Plus tard, lors de la publication, les vérifications de contrat sont désactivées pour maximiser les performances.

Dans de nombreux langages de programmation, les contrats sont implémentés avec assert . Les assertions sont par défaut compilées en mode release en C/C++, et désactivées de la même manière en C# et Java.

Le lancement de l'interpréteur Python avec « -O » (pour « optimiser ») comme argument entraînera également le générateur de code Python à n'émettre aucun bytecode pour les assertions.

Cela élimine efficacement les coûts d’exécution des assertions dans le code de production, indépendamment du nombre et des dépenses de calcul des assertions utilisées dans le développement, car aucune de ces instructions ne sera incluse dans la production par le compilateur.

La conception par contrat ne remplace pas les stratégies de test habituelles, telles que les tests unitaires , les tests d'intégration et les tests système . Elle complète plutôt les tests externes par des auto-tests internes qui peuvent être activés à la fois pour des tests isolés et dans le code de production pendant une phase de test.

L'avantage des autotests internes est qu'ils peuvent détecter les erreurs avant qu'elles ne se manifestent par des résultats non valides observés par le client. Cela conduit à une détection d'erreur plus précoce et plus spécifique.

L'utilisation d'assertions peut être considérée comme une forme d' oracle de test , une manière de tester la conception par la mise en œuvre du contrat.

Les langages qui implémentent la plupart des fonctionnalités DbC de manière native incluent :

• Année 2012
• Salut
• Clojure
• Cobra
• D
• Daphné
• Tour Eiffel
• Forteresse
• Kotlin
• Mercure
• Oxygène (anciennement Chrome et Delphi Prism )
• Racket (y compris les contrats d'ordre supérieur, et soulignant que les violations de contrat doivent blâmer la partie coupable et doivent le faire avec une explication précise )
• Sathe
• Échelle
• SPARK (via l'analyse statique des programmes Ada )
• Vala
• VDM

De plus, la combinaison de méthodes standard dans le système d'objets Common Lisp possède les qualificateurs de méthode :before, :afteret :aroundqui permettent d'écrire des contrats comme méthodes auxiliaires, entre autres utilisations.