Programmation par contrat

La programmation par contrat (en anglais, design by contract ou DBC) 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. 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 quatre 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 pour un invariant de boucle ou un invariant d'objet. Variant : Il s'agit d'une valeur numérique entière positive associée à une boucle. La valeur doit nécessairement décroître à chaque évaluation, garantissant la terminaison. 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.