Méthode B/Concept de précondition

Soit la machine suivante :

MACHINE
   Calculette
...
OPERATIONS
   cc <-- plus (aa, bb) =
   /* avec l'Atelier B, les noms des variables
      et des constantes doivent faire au moins 
      deux caractères */
      PRE
         aa : NAT &
         bb : NAT &
         aa + bb : NAT
      THEN
         cc := aa + bb
      END;
...
END

Quel est le sens de aa + bb : (appartient) ENTIER que l'on trouve dans la précondition ?

- Quand on passera de la machine abstraite au code exécutable, la précondition de l'opération plus ne sera pas présente dans le code exécutable de cette opération.
- La précondition veut dire que, lorsqu'on utilisera la machine abstraite (lorsqu'on l'appellera), si l'on respecte la précondition, la machine se comportera comme spécifiée.
- Si on ne respecte pas la précondition, on n'a aucune garantie de bon fonctionnement.

Exemple de la calculette :

Le concepteur du logiciel démontrera, une fois pour toute, que si la précondition est remplie, la calculette fonctionnera correctement.

ATTENTION :

   Bien différencier l'approche B (programmation offensive) de la programmation défensive !

Exemple de mon enrouleur de câble électrique :

J'ai un enrouleur de câble électrique qui porte l'étiquette suivante : « Puissance maximale sous 200 V = 2000 W avec le câble déroulé, 1000 W avec le câble enroulé. » J'ai utilisé ma tondeuse électrique de 1500 W avec le câble enroulé.

Le câble a fondu.
L'enrouleur ne m'a pas prévenu.
Il ne disposait pas d'un composant testant si le câble était déroulé.
C'est lorsque le fabricant a conçu l'enrouleur qu'il a « démontré » qu'il fonctionne correctement si l'utilisateur respecte les conditions d'emploi écrites sur l'étiquette.

Cette démonstration a été faite une fois pour toute en utilisant les lois de la physique. Le vendeur ne m'a pas remboursé l'enrouleur.

C'est alors à l'utilisateur à ne faire appel à l'enrouleur qu'en respectant les conditions d'emploi. Ces conditions d'emploi ne peuvent être vérifiées dans le « code » de l'opération.