La précondition d'une opération est une condition qui doit être satisfaite avant que l'opération puisse être effectuée.
La postcondition d'une opération est une condition qui doit être satisfaite après que l'opération ait été effectuée.
Donc, prenons quelques opérations et déduisons logiquement leurs pré et postconditions.
- Retrait d'argent d'un compte de débit dans un guichet automatique. La somme retirée doit être inférieure ou égale à la somme restant sur le compte (1ere précondition) et inférieure à la somme restant dans le DAB (2eme précondition). Après avoir retiré l'argent, les rappels d'argent à la fois dans le DAB et sur votre compte doivent être égaux à leur valeur initiale moins la somme retirée (2 postconditions).
- Marier une femme. La précondition est que la femme ne doit pas être déjà mariée (sauf si la polyandrie est légale). La postcondition est qu'après avoir épousé une femme, elle doit se marier (pour que quelqu'un d'autre ne l'épouse pas accidentellement).
- Sortir des éléments de la pile. Précondition : le nombre d'éléments sur une pile doit être supérieur à zéro. Postcondition : le nombre d'éléments sur une pile doit être sa valeur originale moins un et la valeur retournée doit être égale au sommet de la pile.
- Downloading a file. Précondition : le stockage cible doit avoir suffisamment de place pour le fichier et le site de téléchargement doit être accessible. Postcondition : le stockage disponible doit diminuer de la taille du fichier.
- Manger une pizza. Précondition : il y a de la pizza. Postcondition : il n'y a pas de pizza.