Recherchez sur tout Techno-Science.net
       
Techno-Science.net : Suivez l'actualité des sciences et des technologies, découvrez, commentez
 A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | +
Programmation par contrat
Langages à objets
C++ - C# - D
Delphi - Eiffel - Groovy
Java - Lisaac - Python - Ruby
Simula - Smalltalk
Visual Basic - WLangage
Langages impératifs
APL - ASP - Assembleur
BASIC (En programmation, BASIC est un acronyme pour Beginner's All-purpose Symbolic Instruction Code. qui désigne une famille de langages de programmations de haut niveau.) - C - Cobol (COBOL est un langage de programmation de troisième génération créé en 1959 (officiellement le 18 Septembre 1959). Son nom est l'acronyme de COmmon Business Oriented...) - Natural (Natural est un langage de programmation semi-compilé, édité par la société allemande Software AG.)
Forth - Fortran - Limbo
Logo - Pascal - Perl - PHP (PHP (sigle de PHP: Hypertext Preprocessor), est un langage de scripts libre principalement utilisé pour produire des pages Web dynamiques via un serveur HTTP, mais pouvant également fonctionner comme n'importe quel langage...)
Langages fonctionnels
Haskell - ML/OCaml
Lisp/Common Lisp
Scheme - XSLT
Langages déclaratifs
Clips - Prolog
Langages concurrents
Ada 95 - Erlang
Voir aussi
Conception - Codage (De façon générale un codage permet de passer d'une représentation des données vers une autre.)
Tests - Optimisations

La programmation (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 logiciel...) 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 (Le mot client a plusieurs acceptations :) et le fournisseur d'un morceau de code logiciel (En informatique, un logiciel est un ensemble d'informations relatives à des traitements effectués automatiquement par un appareil informatique. Y sont inclus les instructions de traitement, regroupées sous forme de programmes,...). C'est une méthode de programmation semi-formelle dont le but principal est de réduire le nombre (La notion de nombre en linguistique est traitée à l’article « Nombre grammatical ».) de bogues dans les programmes.

Historiquement, la programmation par contrat a été introduite par Bertrand Meyer (Bertrand Meyer (né en 1950 en France) est le créateur du langage de programmation orienté objet Eiffel.) dans son langage Eiffel datant de 1985, qui était inspiré de la notation Z créée par Jean-Raymond Abrial (Jean-Raymond Abrial est un informaticien français, actuellement professeur à l'École polytechnique fédérale de Zurich, connu dans le monde du développement logiciel...).

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 (Dans la langue française, le mot assertion (n,f) représente une vérité absolue : il définit une proposition reconnue comme vraie. -> voir Wiktionary) caractérise l'état interne (En France, ce nom désigne un médecin, un pharmacien ou un chirurgien-dentiste, à la fois en activité et en formation à l'hôpital ou en cabinet pendant une...) de tout (Le tout compris comme ensemble de ce qui existe est souvent interprété comme le monde ou l'univers.) le programme, ou seulement d'une partie comme par exemple pour un invariant de boucle ou un invariant d'objet (De manière générale, le mot objet (du latin objectum, 1361) désigne une entité définie dans un espace à trois...).

Le langage utilisé pour écrire les conditions est important. Il doit avoir une valeur de vérité ; autrement dit c'est une logique (La logique (du grec logikê, dérivé de logos (λόγος), terme inventé par Xénocrate signifiant à la fois raison, langage, et raisonnement) est dans une première approche...) 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 (Le code source (ou les sources voire le source) est un ensemble d'instructions écrites dans un langage de programmation informatique de haut niveau, compréhensible par un être humain...) du programme et permettent de fournir une documentation supplémentaire sur le sens (SENS (Strategies for Engineered Negligible Senescence) est un projet scientifique qui a pour but l'extension radicale de l'espérance de vie humaine. Par une évolution progressive allant du ralentissement du...) que possède le code. Cela permet donc de décrire la sémantique du programme.

Contexte (Le contexte d'un évènement inclut les circonstances et conditions qui l'entourent; le contexte d'un mot, d'une phrase ou d'un texte inclut les...)

Plusieurs langages de programmation implémentent ce paradigme comme Eiffel, D, Lisaac, Spark (Spark est un logiciel libre (GNU LGPL) client de messagerie instantanée pour le réseau standard ouvert Jabber (XMPP) développé en Java.), VDM. Des modules existent pour d'autres langages, comme JContractor pour Java.

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 (Le temps est un concept développé par l'être humain pour appréhender le changement dans le monde.) 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ébuggage.

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 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.

Source: Wikipédia publiée sous licence CC-BY-SA 3.0.

Vous pouvez soumettre une modification à cette définition sur cette page. La liste des auteurs de cet article est disponible ici.