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.