La garde et la précondition

La garde et la précondition

---

H. Habrias
version du 28-05-2002La garde
Considérez cette prise (partie femelle) et la fiche (partie mâle).
 

Il est impossible d'introduire la fiche mâle dans la prise femelle. On a ainsi "implantée" une garde. On se garde de la situation où on pourrait introduire l'une dans l'autre.
Dans "la vie" on utilise aussi des gardiens qui ont pour tâche d'empêcher d'entrer certaines personnes dans un bâtiment. Si vous avez le laisser-passer alors le gardien vous laisse entrer, sinon vous ne pouvez entrer.
 
La précondition
La précondition d'une opération est différente de la garde.
La précondition est une précondition d'emploi. On vous dit : si vous appelez l'opération (si vous faites l'opération) en respectant la précondition, alors l'opération remplira sa fonction. Si vous divisez en respectant la précondition (en ne divisant pas par zéro) alors l'opération remplira sa fonction.
En général, le vendeur vous garantit un produit à condition que vous respectiez les préconditions d'emploi ! Mais il ne vous fournit pas un garde pour vous empêcher d'utiliser le produit hors des conditions d'emploi (hors de la précondition). Vous pouvez très bien ne pas respecter la précondition.
En B, quand on prouve une opération,on prouve que si on appelle une opération sous sa précondition, alors on respecte l'invariant.

Merci à Steve Dunne qui nous a fourni cet exemple pédagogique.