Programmation par contrat


Programmation par contrat

La programmation par contrat est un paradigme de programmation dans lequel le déroulement des traitements est régi par des règles. Ces règles, appelées des assertions, forment un contrat qui précise les responsabilités entre le client et le fournisseur d'un morceau de code logiciel. C'est une méthode de programmation semi-formelle dont le but principal est de réduire le nombre de bugs dans les programmes.

Historiquement, la programmation par contrat a été introduite par Bertrand Meyer dans son langage Eiffel datant de 1985, qui était inspiré de la notation Z créée par Jean-Raymond Abrial.

Sommaire

Principe

Le principe est de préciser ce qui doit être vrai à un moment donné de l'exécution d'un programme. Il ne faut pas penser que ce paradigme oblige à réaliser des tests effectifs des règles pendant l'exécution : ces tests ne sont qu'une des façons de s'assurer que les règles sont respectées. Il existe trois types d'assertions :

  • Précondition : La condition qui doit être vérifiée par le client avant le lancement d'un traitement donné. Cette condition doit garantir que l'exécution du traitement est possible sans erreur.
  • Postcondition : La condition qui doit être garantie par le fournisseur après le déroulement d'un traitement donné. Cette condition doit garantir que le traitement a bien réalisé son travail.
  • Invariant : Il s'agit d'une condition qui est toujours vraie. Selon le type d'invariant, cette assertion caractérise l'état interne de tout le programme, ou seulement d'une partie comme par exemple pour un invariant de boucle ou un invariant d'objet.

Le langage utilisé pour écrire les conditions est important. Il doit avoir une valeur de vérité ; autrement dit c'est une logique et on utilise en général les expressions booléennes du langage hôte. Pour pouvoir exprimer plus de choses on y adjoint souvent un moyen pour que les postconditions puissent se référer à l'ancienne valeur des variables modifiées par le traitement. Enfin on peut rajouter les quantificateurs de la logique du premier ordre.

Ces assertions sont écrites directement dans le code source du programme et permettent de fournir une documentation supplémentaire sur le sens que possède le code. Cela permet donc de décrire la sémantique du programme.

Contexte

Plusieurs langages de programmation implémentent ce paradigme comme Eiffel, D, Lisaac, Spark, VDM. Des modules existent pour d'autres langages, comme OCL pour UML, JContractor pour Java ou PSL pour VHDL.

Cette technique possède un lien très fort avec les méthodes formelles permettant de certifier correct un programme. Les trois règles ci-dessus sont en fait une forme de spécification classique du programme.

Mais, contrairement aux méthodes de preuves de programmes, on ne va pas chercher à montrer explicitement que la spécification est bien réalisée par le programme. Cette partie est laissée à la discrétion du client et du fournisseur.

Néanmoins on met souvent en place des mécanismes de tests des règles pendant l'exécution pour vérifier leur validité. On peut utiliser en plus des tests unitaires pour vérifier les assertions de manière élégante. Mais cela ne permet en aucun cas d'être sûr que les règles sont tout le temps valides. En effet il faudrait, la plupart du temps, réaliser une infinité d'exécutions différentes pour vérifier tous les cas possibles.

Mais il est reconnu que cette méthode permet quand même d'obtenir des logiciels de meilleure qualité et d'accélérer les phases de débogage.

Exemple

Une fonction calculant une racine carrée d'un nombre réel peut être vérifiée de la manière suivante en pseudo code.

  • Fonction calculant la racine carrée de la valeur x
    • Précondition : x ≥ 0
    • Postcondition : résultat ≥ 0 et si x ≠ 1 alors résultat ≠ x

La précondition assure que le développeur utilise la fonction correctement, alors que la postcondition permet au développeur de faire confiance à la fonction.

Voir aussi

Articles connexes

Liens externes


Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Programmation par contrat de Wikipédia en français (auteurs)

Regardez d'autres dictionnaires:

  • Programmation par contrainte — Programmation par contraintes La programmation par contraintes (PPC, ou CP pour Constraint Programming en anglais) consiste à poser un problème sous forme de relations logiques (appelées contraintes) entre plusieurs variables. Un problème formulé …   Wikipédia en Français

  • Programmation par contraintes — La programmation par contraintes (PPC, ou CP pour Constraint Programming en anglais) est un paradigme de programmation apparu dans les années 1980[1],[2] permettant de résoudre des problèmes combinatoires de grandes tailles tels que les problèmes …   Wikipédia en Français

  • Survol de la Programmation par Contraintes — Programmation par contraintes La programmation par contraintes (PPC, ou CP pour Constraint Programming en anglais) consiste à poser un problème sous forme de relations logiques (appelées contraintes) entre plusieurs variables. Un problème formulé …   Wikipédia en Français

  • Programmation — informatique Pour les articles homonymes, voir Programmation (homonymie). La programmation dans le domaine informatique est l ensemble des activités qui permettent l écriture des programmes informatiques. C est une étape importante de la… …   Wikipédia en Français

  • Programmation informatique — Pour les articles homonymes, voir Programmation (homonymie). La programmation dans le domaine informatique est l ensemble des activités qui permettent l écriture des programmes informatiques. C est une étape importante de la conception de… …   Wikipédia en Français

  • Programmation objet — Programmation orientée objet La programmation orientée objet (POO) ou programmation par objet, est un paradigme de programmation informatique qui consiste en la définition et l assemblage de briques logicielles appelées objets ; un objet… …   Wikipédia en Français

  • Programmation orientee objet — Programmation orientée objet La programmation orientée objet (POO) ou programmation par objet, est un paradigme de programmation informatique qui consiste en la définition et l assemblage de briques logicielles appelées objets ; un objet… …   Wikipédia en Français

  • Programmation à objets — Programmation orientée objet La programmation orientée objet (POO) ou programmation par objet, est un paradigme de programmation informatique qui consiste en la définition et l assemblage de briques logicielles appelées objets ; un objet… …   Wikipédia en Français

  • Programmation Orientée Aspect — La programmation orientée aspect (POA, en anglais aspect oriented programming AOP) est un paradigme de programmation qui permet de séparer les considérations techniques (aspect en anglais) des descriptions métier dans une application. Par exemple …   Wikipédia en Français

  • Programmation imperative — Programmation impérative En informatique, la programmation impérative est un paradigme de programmation qui décrit les opérations en termes de séquences d instructions exécutées par l ordinateur pour modifier l état du programme. Sommaire 1… …   Wikipédia en Français


Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.